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.mli | 2 -- 1 file changed, 2 deletions(-) (limited to 'grammar/q_util.mli') 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 -- cgit v1.2.3