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

1 files changed, 6 insertions, 2 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index a8adfb19a..f60d06857 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -31,6 +31,11 @@ let mk_cast = function
     (c,(_,None)) -> c
   | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv (DEFAULTcast, ty))
 
+let binders_of_names l =
+  List.map (fun (loc, na) ->
+    LocalRawAssum ([loc, na], Default Explicit,
+		   CHole (loc, Some (Evd.BinderType na)))) l
+
 let binders_of_lidents l =
   List.map (fun (loc, id) ->
     LocalRawAssum ([loc, Name id], Default Glob_term.Explicit,
@@ -384,8 +389,7 @@ GEXTEND Gram
           [LocalRawAssum (id::idl,Default Explicit,c)]
 	(* binders factorized with open binder *)
       | id = name; idl = LIST0 name; bl = binders ->
-          let t = CHole (loc, Some (Evd.BinderType (snd id))) in
-          LocalRawAssum (id::idl,Default Explicit,t)::bl
+          binders_of_names (id::idl) @ bl
       | id1 = name; ".."; id2 = name ->
           [LocalRawAssum ([id1;(loc,Name ldots_var);id2],
 	                  Default Explicit,CHole (loc,None))]