diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrarg.ml | 3 | ||||
| -rw-r--r-- | interp/constrarg.mli | 2 |
2 files changed, 3 insertions, 2 deletions
diff --git a/interp/constrarg.ml b/interp/constrarg.ml index ab54b6197..44623f9c9 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -49,7 +49,7 @@ let wit_constr_may_eval = let wit_uconstr = Genarg.make0 None "uconstr" -let wit_open_constr = unsafe_of_type OpenConstrArgType +let wit_open_constr = Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) None "open_constr" let wit_constr_with_bindings = Genarg.make0 None "constr_with_bindings" @@ -72,6 +72,7 @@ let () = register_name0 wit_tactic "Constrarg.wit_tactic"; register_name0 wit_sort "Constrarg.wit_sort"; register_name0 wit_uconstr "Constrarg.wit_uconstr"; + register_name0 wit_open_constr "Constrarg.wit_open_constr"; register_name0 wit_constr_may_eval "Constrarg.wit_constr_may_eval"; register_name0 wit_red_expr "Constrarg.wit_red_expr"; register_name0 wit_clause_dft_concl "Constrarg.wit_clause_dft_concl"; diff --git a/interp/constrarg.mli b/interp/constrarg.mli index 052e4ec69..0cc111e61 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -50,7 +50,7 @@ val wit_constr_may_eval : val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type val wit_open_constr : - (open_constr_expr, open_glob_constr, Evd.open_constr) genarg_type + (constr_expr, glob_constr_and_expr, constr) genarg_type val wit_constr_with_bindings : (constr_expr with_bindings, |