From 9ee5808746cbcf6e04c08e6a2e798b6cbb34bb06 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 20 May 2017 21:27:34 +0200
Subject: Fixing a too lax constraint for finding recursive binder part of a
 notation.

This was preventing to work examples such as:

Notation "[ x ; .. ; y ; z ]" := ((x,((fun u => u), .. (y,(fun u =>u,z)) ..))).
---
 interp/notation_ops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 6f91009111..95873ea80d 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -287,7 +287,7 @@ let compare_recursive_parts found f f' (iterator,subc) =
       | Some _ -> false
       end
   | GLambda (Name x,_,t_x,c), GLambda (Name y,_,t_y,term)
-  | GProd (Name x,_,t_x,c), GProd (Name y,_,t_y,term) ->
+  | GProd (Name x,_,t_x,c), GProd (Name y,_,t_y,term) when not (Id.equal x y) ->
       (* We found a binding position where it differs *)
       begin match !diff with
       | None ->
-- 
cgit v1.2.3