Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables a b:A' et 'Variables (a:A) (b:A)'

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

10 files changed, 30 insertions, 31 deletions

diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 29582c382b..8443526930 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -155,7 +155,7 @@ let make_variable_ast name typ implicits =
 let make_variable_ast name typ implicits =
   (VernacAssumption
     ((Local,Definitional),
-     [false,((dummy_loc,name), constr_to_ast (body_of_type typ))]))
+     [false,([dummy_loc,name], constr_to_ast (body_of_type typ))]))
   ::(implicits_to_ast_list implicits);;
     
 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 7cf169ec7d..d2aff445ff 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1281,8 +1281,13 @@ let cvt_optional_eval_for_definition c1 optional_eval =
 	      xlate_formula c1))
 
 let cvt_vernac_binder = function
-  | ((_,id),c) ->
-     CT_binder(CT_id_opt_ne_list (xlate_ident_opt (Some id),[]),xlate_formula c)
+  | (id::idl,c) ->
+     CT_binder(
+       CT_id_opt_ne_list 
+         (xlate_ident_opt (Some (snd id)),
+          List.map (fun id -> xlate_ident_opt (Some (snd id))) idl),
+         xlate_formula c)
+  | ([],_) -> xlate_error "Empty list of vernac binder"
 
 let cvt_vernac_binders args =
   CT_binder_list(List.map cvt_vernac_binder args)
diff --git a/ide/coq.ml b/ide/coq.ml
index c6aa114320..cc060da422 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -317,7 +317,7 @@ let compute_reset_info = function
   | VernacDefineModule ((_,id), _, _, _) 
   | VernacDeclareModule ((_,id), _, _, _)
   | VernacDeclareModuleType ((_,id), _, _)
-  | VernacAssumption (_, (_,((_,id),_))::_)
+  | VernacAssumption (_, (_,((_,id)::_,_))::_)
   | VernacInductive (_, ((_,id),_,_,_,_) :: _) ->
       Reset (id, ref true)
   | VernacDefinition (_, (_,id), ProveBody _, _)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index b1e6cda093..d79b3ec3a8 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -20,9 +20,6 @@ open Vernac_
 open Prim
 open Decl_kinds
 
-(* Dans join_binders, s'il y a un "?", on perd l'info qu'il est partagé *)
-let join_binders (idl,c) = List.map (fun id -> (id,c)) idl
-
 open Genarg
 
 let evar_constr loc = CHole loc
@@ -94,7 +91,7 @@ GEXTEND Gram
 END
 
 let test_plurial_form = function
-  | [_] ->
+  | [_,([_],_)] ->
       Options.if_verbose warning
       "Keywords Variables/Hypotheses/Parameters expect more than one assumption"
   | _ -> ()
@@ -135,12 +132,12 @@ GEXTEND Gram
       | ":" -> false ] ]
   ;
   params:
-    [ [ idl = LIST1 identref SEP ","; coe = of_type_with_opt_coercion; c = constr
-      -> List.map (fun c -> (coe,c)) (join_binders (idl,c))
+    [ [ idl = LIST1 identref SEP ","; coe = of_type_with_opt_coercion; 
+        c = constr -> (coe,(idl,c))
     ] ]
   ;
   ne_params_list:
-    [ [ ll = LIST1 params SEP ";" -> List.flatten ll ] ]
+    [ [ ll = LIST1 params SEP ";" -> ll ] ]
   ;
   name_comma_list_tail:
     [ [ ","; nal = LIST1 name SEP "," -> nal | -> [] ] ]
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 8142303043..8808ef0258 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -86,10 +86,6 @@ let no_coercion loc (c,x) =
     (loc,"no_coercion",Pp.str"no coercion allowed here");
   x
 
-let flatten_assum l =
-  List.flatten
-    (List.map (fun (oc,(idl,t)) -> List.map (fun id -> (oc,(id,t))) idl) l)
-
 (* Gallina declarations *)
 if not !Options.v7 then
 GEXTEND Gram
@@ -104,11 +100,10 @@ GEXTEND Gram
       | (f,d) = def_token; id = identref; b = def_body -> 
           VernacDefinition (d, id, b, f)
       | stre = assumption_token; bl = assum_list -> 
-	  VernacAssumption (stre, flatten_assum bl)
+	  VernacAssumption (stre, bl)
       | stre = assumptions_token; bl = assum_list ->
-	  let l = flatten_assum bl in
-	  test_plurial_form l;
-	  VernacAssumption (stre, l)
+	  test_plurial_form bl;
+	  VernacAssumption (stre, bl)
       (* Gallina inductive declarations *)
       | f = finite_token;
         indl = LIST1 inductive_definition SEP "with" ->
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 44d1bfa1e7..ea38340cea 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -147,9 +147,7 @@ let syntax_definition ident c =
 let assumption_message id =
   if_verbose message ((string_of_id id) ^ " is assumed")
 
-let declare_assumption ident is_coe (local,kind) bl c =
-  let c = prod_rawconstr c bl in
-  let c = interp_type Evd.empty (Global.env()) c in
+let declare_one_assumption is_coe (local,kind) c (_,ident) =
   let r = match local with
     | Local when Lib.sections_are_opened () ->
         let r = 
@@ -170,6 +168,11 @@ let declare_assumption ident is_coe (local,kind) bl c =
         ConstRef kn in
   if is_coe then Class.try_add_new_coercion r local
 
+let declare_assumption idl is_coe k bl c =
+  let c = prod_rawconstr c bl in
+  let c = interp_type Evd.empty (Global.env()) c in
+  List.iter (declare_one_assumption is_coe k c) idl
+
 (* 3a| Elimination schemes for mutual inductive definitions *)
 
 open Indrec
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 07faea0b04..db5ab27b09 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -35,8 +35,8 @@ val declare_definition : identifier -> definition_kind ->
 
 val syntax_definition : identifier -> constr_expr -> unit
 
-val declare_assumption : identifier -> coercion_flag -> assumption_kind -> 
-  local_binder list -> constr_expr -> unit
+val declare_assumption : identifier located list ->
+  coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> unit
 
 val build_mutual : inductive_expr list -> bool -> unit
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 58eb42b6d0..91c23fb7a3 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -297,8 +297,7 @@ let vernac_exact_proof c =
   save_named true
 
 let vernac_assumption kind l =
-  List.iter (fun (is_coe,((_,id),c)) ->
-              declare_assumption id is_coe kind [] c) l
+  List.iter (fun (is_coe,(idl,c)) -> declare_assumption idl is_coe kind [] c) l
 
 let vernac_inductive f indl = build_mutual indl f
 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 9fd934d563..7b1203e57b 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -136,9 +136,9 @@ type inductive_flag = bool (* true = Inductive;     false = CoInductive    *)
 type sort_expr = Rawterm.rawsort
 
 type decl_notation = (string * constr_expr * scope_name option) option
-type simple_binder = lident * constr_expr
+type simple_binder = lident list  * constr_expr
 type 'a with_coercion = coercion_flag * 'a
-type constructor_expr = simple_binder with_coercion
+type constructor_expr = (lident * constr_expr) with_coercion
 type inductive_expr =
      lident * decl_notation * local_binder list * constr_expr
     * constructor_expr list
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 6756e3157f..c60e5d87ca 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -360,10 +360,10 @@ let pr_params pr_c (xl,(c,t)) =
 
 let rec factorize = function
   | [] -> []
-  | (c,(x,t))::l ->
+  | (c,(idl,t))::l ->
       match factorize l with
-	| (xl,t')::l' when t' = (c,t) -> (x::xl,t')::l'
-	| l' -> ([x],(c,t))::l'
+	| (xl,t')::l' when t' = (c,t) -> (idl@xl,t')::l'
+	| l' -> (idl,(c,t))::l'
 
 let pr_ne_params_list pr_c l =
   match factorize l with