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. --- test-suite/bugs/closed/5696.v | 5 +++++ test-suite/bugs/closed/7903.v | 4 ++++ 2 files changed, 9 insertions(+) create mode 100644 test-suite/bugs/closed/5696.v create mode 100644 test-suite/bugs/closed/7903.v (limited to 'test-suite') diff --git a/test-suite/bugs/closed/5696.v b/test-suite/bugs/closed/5696.v new file mode 100644 index 000000000..a20ad1b4d --- /dev/null +++ b/test-suite/bugs/closed/5696.v @@ -0,0 +1,5 @@ +(* Slightly improving interpretation of Ltac subterms in notations *) + +Notation "'var2' x .. y = z ; e" := (ltac:(exact z), (fun x => .. (fun y => e) +..)) (at level 200, x binder, y binder, e at level 220). +Check (var2 a = 1; a). diff --git a/test-suite/bugs/closed/7903.v b/test-suite/bugs/closed/7903.v new file mode 100644 index 000000000..55c7ee99a --- /dev/null +++ b/test-suite/bugs/closed/7903.v @@ -0,0 +1,4 @@ +(* Slightly improving interpretation of Ltac subterms in notations *) + +Notation bar x f := (let z := ltac:(exact 1) in (fun x : nat => f)). +Check bar x (x + x). -- cgit v1.2.3