From 63f3ca8973a877f22db4d5fea541c1fab1b706f2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 18 Jul 2016 21:15:23 +0200
Subject: Removing a source of clash with multiple recursive patterns in
 notations.

The same variable name was used to collect the binders and the
successive steps of matching one binder, resulting in unexpected
attempts for merging in the presence of multiple occurrence of the
same recursive pattern.

An amusing side-effect: when eta-expanding for a notation with
recursive binders, it is the second variable of the "x .. y" which is
used to invent a name rather than the first one.
---
 test-suite/output/Notations2.out | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index d9ce42c606..20101f48e5 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -12,7 +12,7 @@ let '(a, _, _) := (2, 3, 4) in a
      : nat
 exists myx y : bool, myx = y
      : Prop
-fun (P : nat -> nat -> Prop) (x : nat) => exists x0, P x x0
+fun (P : nat -> nat -> Prop) (x : nat) => exists y, P x y
      : (nat -> nat -> Prop) -> nat -> Prop
 ∃ n p : nat, n + p = 0
      : Prop
-- 
cgit v1.2.3