From 90e5945e1666540bc18e7a9b831d136041f4e487 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 12 Sep 2016 17:22:03 +0200
Subject: Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.

---
 interp/notation_ops.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 5abc7794bd..ec4b2e9386 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -577,7 +577,8 @@ let rec alpha_var id1 id2 = function
 
 let add_env alp (sigma,sigmalist,sigmabinders) var v =
   (* Check that no capture of binding variables occur *)
-  if List.exists (fun (id,_) ->occur_glob_constr id v) alp then raise No_match;
+  if not (Id.equal ldots_var var) &&
+     List.exists (fun (id,_) -> occur_glob_constr id v) alp then raise No_match;
   (* TODO: handle the case of multiple occs in different scopes *)
   ((var,v)::sigma,sigmalist,sigmabinders)
 
-- 
cgit v1.2.3