diff options
| -rw-r--r-- | interp/stdarg.ml | 2 | ||||
| -rw-r--r-- | ltac/extratactics.ml4 | 8 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 1 |
3 files changed, 3 insertions, 8 deletions
diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 9e85dbaf38..2a7d52e3af 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -27,7 +27,7 @@ let wit_string : string uniform_genarg_type = make0 "string" let wit_pre_ident : string uniform_genarg_type = - make0 "preident" + make0 ~dyn:(val_tag (topwit wit_string)) "preident" (** Aliases for compatibility *) diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index eda530c265..925c1679f2 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -938,12 +938,6 @@ type cmp = type 'i test = | Test of cmp * 'i * 'i -let wit_cmp : (cmp,cmp,cmp) Genarg.genarg_type = Genarg.make0 "cmp" -let _ = Geninterp.register_val0 wit_cmp None -let wit_test : (int or_var test,int or_var test,int test) Genarg.genarg_type = - Genarg.make0 "tactest" -let _ = Geninterp.register_val0 wit_test None - let pr_cmp = function | Eq -> Pp.str"=" | Lt -> Pp.str"<" @@ -966,7 +960,7 @@ let pr_itest' _prc _prlc _prt = pr_itest -ARGUMENT EXTEND comparison TYPED AS cmp PRINTED BY pr_cmp' +ARGUMENT EXTEND comparison PRINTED BY pr_cmp' | [ "=" ] -> [ Eq ] | [ "<" ] -> [ Lt ] | [ "<=" ] -> [ Le ] diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index e93c395e3d..0ba18f568a 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -65,6 +65,7 @@ let pr_fun_ind_using_typed prc prlc _ opt_c = ARGUMENT EXTEND fun_ind_using + TYPED AS constr_with_bindings option PRINTED BY pr_fun_ind_using_typed RAW_TYPED AS constr_with_bindings_opt RAW_PRINTED BY pr_fun_ind_using |