diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2013-12-01 17:11:44 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2013-12-01 17:14:27 +0100 |
| commit | 233a782a2336f003869f82e697a567ed02885f23 (patch) | |
| tree | 47032c60ff57e6d423f28dc4f2f6b228194a4370 /tactics | |
| parent | e875e90d1d90aec22e6f206f04c4941cb5a3bcd1 (diff) | |
Ensuring the right parsing of glob arguments, used by refine
and instantiate. Each of these tactics uses it at a different
parsing level, thus actually triggering a parsing error after
merging them. This fix implies some code duplication, which is
a pity. The separation between genargs and parsing entries should
be made one day.
Diffstat (limited to 'tactics')
| -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 a3c531f80..c156e869d 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 1367f7032..dfc14bddf 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 2e753e0cc..031cbc7c5 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 |