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).

---
 interp/notation_ops.ml            |  4 +++-
 test-suite/bugs/closed/bug_8794.v | 11 +++++++++++
 2 files changed, 14 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/bug_8794.v

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index ab57176643..7a525f84a5 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -892,7 +892,9 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma)
     | GVar id' ->
        (if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp),
        sigma
-    | _ -> anomaly (str "A term which can be a binder has to be a variable.")
+    | t ->
+       (* The term is a non-variable pattern *)
+       raise No_match
   with Not_found ->
     (* The matching against a term allowing to find the instance has not been found yet *)
     (* If it will be a different name, we shall unfortunately fail *)
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