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

1 files changed, 30 insertions, 4 deletions

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 1d63486ba..bb3027aa8 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