diff options
| author | Pierre-Marie Pédrot | 2016-09-15 16:09:17 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-09-15 16:33:00 +0200 |
| commit | 975e7cd2ad032668c7df690c9bdaa8cdbb196569 (patch) | |
| tree | d7c511f083288601aa3fee1032b76834f28913d8 /interp/constrarg.ml | |
| parent | 21dc493a93853525c5d9c33c0c7558909ce5e79d (diff) | |
Moving Ltac-specific generic arguments to their own file in the ltac/ folder.
Diffstat (limited to 'interp/constrarg.ml')
| -rw-r--r-- | interp/constrarg.ml | 11 |
1 files changed, 1 insertions, 10 deletions
diff --git a/interp/constrarg.ml b/interp/constrarg.ml index ca828102b9..aaf33a956a 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -7,7 +7,6 @@ (************************************************************************) open Loc -open Tacexpr open Misctypes open Genarg open Geninterp @@ -27,14 +26,9 @@ let loc_of_or_by_notation f = function let wit_int_or_var = make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) "int_or_var" -let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type = +let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, Tacexpr.glob_constr_and_expr intro_pattern_expr located, Tacexpr.intro_pattern) genarg_type = make0 "intropattern" -let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type = - make0 "tactic" - -let wit_ltac = make0 ~dyn:(val_tag (topwit Stdarg.wit_unit)) "ltac" - let wit_ident = make0 "ident" @@ -61,9 +55,6 @@ let wit_red_expr = make0 "redexpr" let wit_clause_dft_concl = make0 "clause_dft_concl" -let wit_destruction_arg = - make0 "destruction_arg" - (** Aliases *) let wit_reference = wit_ref |