Construct "T with (Definition|Module) id := c" generalized to

"T with (Definition|Module) M1.M2....Mn.id := c" (in the ML style).


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

5 files changed, 41 insertions, 8 deletions

diff --git a/kernel/entries.ml b/kernel/entries.ml
index 504c11fdfb..6ea4bfc591 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -85,8 +85,8 @@ and module_type_entry =
 and module_signature_entry = (label * specification_entry) list
 
 and with_declaration = 
-    With_Module of identifier * module_path
-  | With_Definition of identifier * constr
+    With_Module of identifier list * module_path
+  | With_Definition of identifier list * constr
 
 and module_expr = 
     MEident of module_path
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 4b4cee03ab..71c756e260 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -85,8 +85,8 @@ and module_type_entry =
 and module_signature_entry = (label * specification_entry) list
 
 and with_declaration = 
-    With_Module of identifier * module_path
-  | With_Definition of identifier * constr
+    With_Module of identifier list * module_path
+  | With_Definition of identifier list * constr
 
 and module_expr = 
     MEident of module_path
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 1d63486ba1..bb3027aa8b 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -66,8 +66,9 @@ and merge_with env mtb with_decl =
     | MTBsig(msid,sig_b) -> msid,sig_b 
     | _ -> error_signature_expected mtb
   in
-  let id = match with_decl with 
-    | With_Definition (id,_) | With_Module (id,_) -> id
+  let id,idl = match with_decl with 
+    | With_Definition (id::idl,_) | With_Module (id::idl,_) -> id,idl
+    | With_Definition ([],_) | With_Module ([],_) -> assert false
   in
   let l = label_of_id id in
     try
@@ -75,7 +76,9 @@ and merge_with env mtb with_decl =
       let before = List.rev rev_before in
       let env' = Modops.add_signature (MPself msid) before env in
       let new_spec = match with_decl with
-	| With_Definition (id,c) -> 
+        | With_Definition ([],_)
+        | With_Module ([],_) -> assert false
+	| With_Definition ([id],c) -> 
 	    let cb = match spec with
 		SPBconst cb -> cb
 	      | _ -> error_not_a_constant l
@@ -107,7 +110,7 @@ and merge_with env mtb with_decl =
                                     const_constraints = cst}
 	      end	
 (* and what about msid's ????? Don't they clash ? *)
-	| With_Module (id, mp) ->
+	| With_Module ([id], mp) ->
 	    let old = match spec with
 		SPBmodule msb -> msb
 	      | _ -> error_not_a_module (string_of_label l)
@@ -138,6 +141,29 @@ and merge_with env mtb with_decl =
 	       msb_constraints = Constraint.union old.msb_constraints cst }
 	    in
 	      SPBmodule msb
+	| With_Definition (_::_,_)
+        | With_Module (_::_,_) -> 
+	    let old = match spec with
+		SPBmodule msb -> msb
+	      | _ -> error_not_a_module (string_of_label l)
+	    in
+	      begin
+		match old.msb_equiv with
+                   None ->
+                    let new_with_decl = match with_decl with
+                       With_Definition (_,c) -> With_Definition (idl,c)
+                     | With_Module (_,c) -> With_Module (idl,c) in
+                    let modtype = 
+                     merge_with env' old.msb_modtype new_with_decl in
+                    let msb =
+	              {msb_modtype = modtype; 
+	               msb_equiv = None; 
+	               msb_constraints = old.msb_constraints }
+	            in
+	             SPBmodule msb
+                 | Some mp ->
+                    error_a_generative_module_expected l
+              end
       in
 	MTBsig(msid,  before@(l,new_spec)::after)
     with
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 744da223a9..390461d5a0 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -67,6 +67,11 @@ let error_not_a_constant l =
 let error_with_incorrect l =
   error ("Incorrect constraint for label \""^(string_of_label l)^"\"")
 
+let error_a_generative_module_expected l =
+  error ("The module " ^ string_of_label l ^ " is not generative. Only " ^
+         "component of generative modules can be changed using the \"with\" " ^
+         "construct.")
+
 let error_local_context lo = 
   match lo with
       None -> 
diff --git a/kernel/modops.mli b/kernel/modops.mli
index e770edc93e..052bac2430 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -92,6 +92,8 @@ val error_not_a_constant : label -> 'a
 
 val error_with_incorrect : label -> 'a
 
+val error_a_generative_module_expected : label -> 'a
+
 val error_local_context : label option -> 'a
 
 val error_circular_with_module : identifier -> 'a