diff options
| author | ppedrot | 2013-07-02 17:28:22 +0000 |
|---|---|---|
| committer | ppedrot | 2013-07-02 17:28:22 +0000 |
| commit | 556c2ce6f1b09d09484cc83f6ada213496add45b (patch) | |
| tree | fe48802a1c5876c42c9ed03dbb6d876030bf2aac /interp | |
| parent | 89abe2a141b3baa11bf0e8bcdecaf68220251c6e (diff) | |
Removing the use of leveled tactics wit_tacticn. It is now handled
through a unique generic argument, and the level is only considered
at parsing time.
This may introduce unnecessary parentheses in Ltac printing though,
as every tactic argument is collapsed at the lowest level. I assume
this does not matter that much, and anyway Ltac printing is quite
bugged as of today.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16616 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |