diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrarg.ml | 4 | ||||
| -rw-r--r-- | interp/constrarg.mli | 3 |
2 files changed, 7 insertions, 0 deletions
diff --git a/interp/constrarg.ml b/interp/constrarg.ml index 37e627a6d4..c25e02c02c 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -55,6 +55,9 @@ let wit_bindings = unsafe_of_type BindingsArgType let wit_red_expr = unsafe_of_type RedExprArgType +let wit_clause_dft_concl = + Genarg.make0 None "clause_dft_concl" + (** Register location *) let () = @@ -62,3 +65,4 @@ let () = register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern"; register_name0 wit_tactic "Constrarg.wit_tactic"; register_name0 wit_sort "Constrarg.wit_sort"; + register_name0 wit_clause_dft_concl "Constrarg.wit_clause_dft_concl"; diff --git a/interp/constrarg.mli b/interp/constrarg.mli index 5faef378a6..d5d19f2eaa 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -30,6 +30,7 @@ val wit_int_or_var : int or_var uniform_genarg_type val wit_intro_pattern : intro_pattern_expr located uniform_genarg_type + val wit_ident : Id.t uniform_genarg_type val wit_var : (Id.t located, Id.t located, Id.t) genarg_type @@ -68,3 +69,5 @@ val wit_red_expr : (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type val wit_tactic : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type + +val wit_clause_dft_concl : (Names.Id.t Loc.located Tacexpr.or_metaid Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type |