From 8d9b66bed22364f513771e9b1fa3df14a3dab866 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 26 Jun 2018 11:50:21 +0200 Subject: Ad hoc fix for #5696, #7903 (ltac subterms and open subterms in notations). We fix the issue by removing terms of the substitutions which have free variables and are thus not interpretable in the context of the "ltac:" subterm. This remains rather ad hoc, since, in an expression "Notation f x := ltac:(foo)", we interpret "x" at calling time of "foo" rather than at use time of "x" in foo, even if "x" is not necessary. We could also imagine that binders in the ltac expressions are then interpreted but that would start to be (very) complicated. Note that this will presumably "fix" ltac2 quotations at the same time. --- interp/constrintern.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 4e217b2cd..18d6c1a5b 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -710,10 +710,12 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = let arg = match arg with | None -> None | Some arg -> - let mk_env (c, (tmp_scope, subscopes)) = + let mk_env id (c, (tmp_scope, subscopes)) map = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in - let gc = intern nenv c in - (gc, Some c) + try + let gc = intern nenv c in + Id.Map.add id (gc, Some c) map + with GlobalizationError _ -> map in let mk_env' (c, (onlyident,(tmp_scope,subscopes))) = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in @@ -725,7 +727,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = | [pat] -> (glob_constr_of_cases_pattern pat, None) | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.loc () in - let terms = Id.Map.map mk_env terms in + let terms = Id.Map.fold mk_env terms Id.Map.empty in let binders = Id.Map.map mk_env' binders in let bindings = Id.Map.fold Id.Map.add terms binders in Some (Genintern.generic_substitute_notation bindings arg) -- cgit v1.2.3