diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-14 19:51:46 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-14 19:51:46 +0200 |
| commit | b161ad97fdc01ac8816341a089365657cebc6d2b (patch) | |
| tree | fe82ae4aa65c6c7bc175f75d7e8ab0b6572dd0f8 /grammar | |
| parent | bd0befffb80c3086e3b451456cec24f3a12ac1f0 (diff) | |
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.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/q_util.ml4 | 3 | ||||
| -rw-r--r-- | grammar/q_util.mli | 2 | ||||
| -rw-r--r-- | grammar/tacextend.ml4 | 5 |
3 files changed, 5 insertions, 5 deletions
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4 index 53330429d..a9a339241 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 a34fc0bcb..9b6f11827 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 19b6e1b5f..4c4ecaf73 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 -> |