diff options
| -rw-r--r-- | tactics/extraargs.ml4 | 14 | ||||
| -rw-r--r-- | tactics/extraargs.mli | 7 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 2 |
3 files changed, 22 insertions, 1 deletions
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index a3c531f80a..c156e869da 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -119,6 +119,20 @@ ARGUMENT EXTEND glob [ constr(c) ] -> [ c ] END +ARGUMENT EXTEND lglob + PRINTED BY pr_globc + + INTERPRETED BY interp_glob + GLOBALIZED BY glob_glob + SUBSTITUTED BY subst_glob + + RAW_TYPED AS constr_expr + RAW_PRINTED BY pr_gen + + GLOB_TYPED AS glob_constr_and_expr + GLOB_PRINTED BY pr_gen + [ lconstr(c) ] -> [ c ] +END type 'id gen_place= ('id * hyp_location_flag,unit) location diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index 1367f70324..dfc14bddf3 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -28,7 +28,14 @@ val wit_glob : (constr_expr, Tacexpr.glob_constr_and_expr, Tacinterp.interp_sign * glob_constr) Genarg.genarg_type + +val wit_lglob : + (constr_expr, + Tacexpr.glob_constr_and_expr, + Tacinterp.interp_sign * glob_constr) Genarg.genarg_type + val glob : constr_expr Pcoq.Gram.entry +val lglob : constr_expr Pcoq.Gram.entry type 'id gen_place= ('id * Locus.hyp_location_flag,unit) location diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 2e753e0cce..031cbc7c5d 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -431,7 +431,7 @@ END open Tacticals TACTIC EXTEND instantiate - [ "instantiate" "(" integer(i) ":=" glob(c) ")" hloc(hl) ] -> + [ "instantiate" "(" integer(i) ":=" lglob(c) ")" hloc(hl) ] -> [ Proofview.V82.tactic (instantiate i c hl) ] | [ "instantiate" ] -> [ Proofview.V82.tactic (tclNORMEVAR) ] END |