From b161ad97fdc01ac8816341a089365657cebc6d2b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 14 May 2016 19:51:46 +0200
Subject: Hack in TACTIC EXTEND to maintain the 8.5 behaviour on badly designed
 arguments.

Since TACTIC EXTEND relies on the usual tactic notation mechanism, the
interpretation of an ML tactic first goes through a TacAlias node. This
means that variables bound by the notation overwrite those of the current
environment. It turns out to be problematic for badly designed arguments
that close over variables of the environment, e.g. glob_constr, because
the variables used at interpretation time are now different from the ones
of parsing time.

Ideally, those arguments should return a closure made of the inner argument
together with the Ltac environment they were defined in. Unluckily, this would
need some important changes in their design. Most notably, most of ssreflect
ARGUMENT EXTEND actually create such closed arguments.

In order to emulate the old behaviour, we rather use a hack by prefixing
ML-bound variables by a character that is not accessible from user-side.
---
 grammar/q_util.ml4    | 3 ---
 grammar/q_util.mli    | 2 --
 grammar/tacextend.ml4 | 5 +++++
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index 53330429d9..a9a339241e 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -58,9 +58,6 @@ let mlexpr_of_option f = function
   | None -> <:expr< None >>
   | Some e -> <:expr< Some $f e$ >>
 
-let mlexpr_of_ident id =
-  <:expr< Names.Id.of_string $str:id$ >>
-
 let symbol_of_string s = <:expr< Extend.Atoken (CLexer.terminal $str:s$) >>
 
 let rec mlexpr_of_prod_entry_key f = function
diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index a34fc0bcb7..9b6f11827c 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -41,8 +41,6 @@ val mlexpr_of_string : string -> MLast.expr
 
 val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr
 
-val mlexpr_of_ident : string -> MLast.expr
-
 val mlexpr_of_prod_entry_key : (string -> MLast.expr) -> user_symbol -> MLast.expr
 
 val type_of_user_symbol : user_symbol -> argument_type
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 19b6e1b5f6..4c4ecaf732 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -18,6 +18,11 @@ let dloc = <:expr< Loc.ghost >>
 
 let plugin_name = <:expr< __coq_plugin_name >>
 
+let mlexpr_of_ident id =
+  (** Workaround for badly-designed generic arguments lacking a closure *)
+  let id = "$" ^ id in
+  <:expr< Names.Id.of_string_soft $str:id$ >>
+
 let rec make_patt = function
   | [] -> <:patt< [] >>
   | ExtNonTerminal (_, p) :: l ->
-- 
cgit v1.2.3