Fixing a few bugs (see #2571) related to interpretation of multiple binders

- fixing missing spaces in the format of the exists' notations (Logic.v);
- fixing wrong variable name in check_is_hole error message (topconstr.ml);
- interpret expressions with open binders such as "forall x y, t" as
  "forall (x:_) (y:_),t" instead of "forall (x y:_),t" to avoid
  the "implicit type" of a variable being propagated to the type of
  another variable of different base name.

An open question remains: when writing explicitly "forall (x y:_),t",
should the types of x and y be the same or not. To avoid the "bug"
that x and y have implicit types but the one of x takes precedences, I
enforced the interpretation (in constrintern, not in parsing) that
"forall (x y:_),t" means the same as "forall (x:_) (y:_),t". However,
another choice could have been made. Then one would have to check that
if x and y have implicit types, they are the same; also, glob_constr
should ideally be changed to support a GProd and GLam with multiple
names in the same type, especially if this type is an evar. On the
contrary, one might also want e.g. "forall x y : list _, t" to mean
"forall (x:list _) (y:list _), t" with distinct instanciations of
"_" ...).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15121 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 7 insertions, 0 deletions

diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 3b3351d33..cf45025ea 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -10,6 +10,8 @@ end
      : nat
 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
      : (nat -> nat -> Prop) -> nat -> Prop
 ∃ n p : nat, n + p = 0
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 1fcbe858a..e53c94ef0 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -25,6 +25,11 @@ Remove Printing Let prod.
 Check match (0,0,0) with (x,y,z) => x+y+z end.
 Check let '(a,b,c) := ((2,3),4) in a.
 
+(* Check printing of notations with mixed reserved binders (see bug #2571) *)
+
+Implicit Type myx : bool.
+Check exists myx y, myx = y.
+
 (* Test notation for anonymous functions up to eta-expansion *)
 
 Check fun P:nat->nat->Prop => fun x:nat => ex (P x).