diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-26 11:50:21 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-26 22:31:10 +0200 |
| commit | 8d9b66bed22364f513771e9b1fa3df14a3dab866 (patch) | |
| tree | 680754acfbb0234bd66a7245a5d2a4b51085de7c /test-suite | |
| parent | a1fc621b943dbf904705dc88ed27c26daf4c5e72 (diff) | |
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.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/5696.v | 5 | ||||
| -rw-r--r-- | test-suite/bugs/closed/7903.v | 4 |
2 files changed, 9 insertions, 0 deletions
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). |