From 4cddb7d0765a091c6514a85475dcdd7af34aaf29 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 1 Mar 2014 16:34:54 +0100
Subject: Never suppress the typing constraint of bound variables whose name
 was reserved with Implicit Type.

---
 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 b42ef2c511..958001c39f 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -10,7 +10,7 @@ end
      : nat
 let '(a, _, _) := (2, 3, 4) in a
      : nat
-exists myx (y : bool), myx = y
+exists myx y : bool, myx = y
      : Prop
 fun (P : nat -> nat -> Prop) (x : nat) => exists x0, P x x0
      : (nat -> nat -> Prop) -> nat -> Prop
-- 
cgit v1.2.3