Module Ltac_plugin.G_eqdecide