diff options
Diffstat (limited to 'test-suite/bugs/closed/8672.v')
| -rw-r--r-- | test-suite/bugs/closed/8672.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/8672.v b/test-suite/bugs/closed/8672.v new file mode 100644 index 00000000..66cd6dfa --- /dev/null +++ b/test-suite/bugs/closed/8672.v @@ -0,0 +1,5 @@ +(* Was generating a dangling "pat" variable at some time *) + +Notation "'plet' x := e 'in' t" := + ((fun H => let x := id H in t) e) (at level 0, x pattern). +Definition bla := plet (pair x y) := pair 1 2 in x. |