From c76fbecdfe4231ee3e0753c0efe665b1e8a8bba5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 23 Oct 2018 15:59:00 +0200
Subject: Fixing #8794 (anomaly with abbreviation involving both term and
 binders).

---
 test-suite/bugs/closed/bug_8794.v | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_8794.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_8794.v b/test-suite/bugs/closed/bug_8794.v
new file mode 100644
index 0000000000..5ff0b30260
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8794.v
@@ -0,0 +1,11 @@
+(* This used to raise an anomaly in 8.8 *)
+
+Inductive T := Tau (t : T).
+
+Notation idT t := (match t with Tau t => Tau t end).
+
+Lemma match_itree : forall (t : T), t = idT t.
+Proof. destruct t; auto. Qed.
+
+Lemma what (k : unit -> T) : k tt = k tt.
+Proof. rewrite match_itree. Abort.
-- 
cgit v1.2.3