diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrarg.ml | 8 | ||||
| -rw-r--r-- | interp/constrarg.mli | 2 |
2 files changed, 9 insertions, 1 deletions
diff --git a/interp/constrarg.ml b/interp/constrarg.ml index 87da56e4fc..5c2b3392c4 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -14,6 +14,7 @@ open Libnames open Globnames open Glob_term open Genredexpr +open Tacexpr open Pattern open Constrexpr open Term @@ -35,6 +36,9 @@ let wit_int_or_var = unsafe_of_type IntOrVarArgType let wit_intro_pattern : intro_pattern_expr located uniform_genarg_type = Genarg.make0 None "intropattern" +let wit_tactic : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type = + Genarg.make0 None "tactic" + let wit_ident_gen b = unsafe_of_type (IdentArgType b) let wit_ident = wit_ident_gen true @@ -69,4 +73,6 @@ let wit_red_expr = unsafe_of_type RedExprArgType (** Register location *) -let () = register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern" +let () = + register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern"; + register_name0 wit_tactic "Constrarg.wit_tactic" diff --git a/interp/constrarg.mli b/interp/constrarg.mli index 548bd66905..1233e165fd 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -77,3 +77,5 @@ val wit_red_expr : ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, (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 |