Merge PR #8806: Fixing #8794: anomaly with abbreviation binding both a term and a binder

2 files changed, 14 insertions, 1 deletions

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.