Ltac_plugin.Extratactics
type cmp =
| Eq
| Lt
| Le
| Gt
| Ge
val wit_comparison : (cmp, cmp, cmp) Genarg.genarg_type
type 'i test =
| Test of cmp * 'i * 'i
val wit_test : (int Locus.or_var test, int Locus.or_var test, int test) Genarg.genarg_type