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 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'interp/notation_ops.ml')

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 *)
-- 
cgit v1.2.3