From 233a782a2336f003869f82e697a567ed02885f23 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 1 Dec 2013 17:11:44 +0100
Subject: 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.

---
 tactics/extraargs.ml4    | 14 ++++++++++++++
 tactics/extraargs.mli    |  7 +++++++
 tactics/extratactics.ml4 |  2 +-
 3 files changed, 22 insertions(+), 1 deletion(-)

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
-- 
cgit v1.2.3