Correction bug 1979.

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

2 files changed, 90 insertions, 70 deletions

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index afde8d557c..f4f52d83dd 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -37,6 +37,11 @@ let rec list_fold_map2 f e = function
        let e'',t1',t2' = list_fold_map2 f e' t in
 	 e'',h1'::t1',h2'::t2'
 
+let rec rebuild_mp mp l =
+  match l with
+      []-> mp
+    | i::r -> rebuild_mp (MPdot(mp,i)) r 
+	
 let type_of_struct env b meb = 
   let rec aux env = function 
   | SEBfunctor (mp,mtb,body) ->
@@ -191,37 +196,48 @@ and check_with_aux_mod env mtb with_decl now =
 	      in
 		if now then 
 		  let mp' = scrape_alias mp env' in
-		  let up_subst = update_subst mtb'.typ_alias (map_mp (mp_rec [id]) mp') in
+		  let _,sub = Modops.update_subst env' (module_body_of_type mtb') mp' in
+		  let up_subst = update_subst sub (map_mp (mp_rec [id]) mp') in
 		    cst, (join (map_mp (mp_rec [id]) mp') up_subst),(return_opt_type mp env' mtb')
 		else
 		cst,empty_subst,(return_opt_type mp env' mtb')
         | With_Module (_::_,mp) -> 
-	    let old = match spec with
-		SFBmodule msb -> msb
+	    let old,alias = match spec with
+		SFBmodule msb -> Some msb, None
+	      | SFBalias (mpold,typ_opt,cst)->None, Some mpold
 	      | _ -> error_not_a_module (string_of_label l)
 	    in
 	      begin
-		match old.mod_expr 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 cst,_,typ_opt =
-			check_with_aux_mod env' 
-			  (type_of_mb env' old) new_with_decl false in
-			if now then 
-			  let mtb' = lookup_modtype mp env' in
-			  let mp' = scrape_alias mp env' in
-			  let up_subst = update_subst 
-			    mtb'.typ_alias (map_mp (mp_rec (List.rev (id::idl))) mp') in
-			    cst, 
-		      (join (map_mp (mp_rec (List.rev (id::idl))) mp') up_subst),
-		      typ_opt
+		if alias = None then
+		  let old = Option.get old in
+		    match old.mod_expr 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 cst,_,typ_opt =
+			    check_with_aux_mod env' 
+			      (type_of_mb env' old) new_with_decl false in
+			    if now then 
+			    let mtb' = lookup_modtype mp env' in
+			    let mp' = scrape_alias mp env' in
+			    let _,sub = Modops.update_subst env' (module_body_of_type mtb') mp' in
+			    let up_subst = update_subst 
+			      sub (map_mp (mp_rec (List.rev (id::idl))) mp') in
+			      cst, 
+			  (join (map_mp (mp_rec (List.rev (id::idl))) mp') up_subst),
+			  typ_opt
+			    else
+			      cst,empty_subst,typ_opt
+		      | Some msb ->
+			  error_a_generative_module_expected l
 		else
-		cst,empty_subst,typ_opt
-		  | Some msb ->
-                      error_a_generative_module_expected l
+		  let mpold =  Option.get alias in 
+		  let mpnew = rebuild_mp mpold (List.map label_of_id idl) in
+		    check_modpath_equiv env' mpnew mp;
+		    let mtb' = lookup_modtype mp env' in
+		      Constraint.empty,empty_subst,(return_opt_type mp env' mtb')
               end
 	| _ -> anomaly "Modtyping:incorrect use of with"
     with
diff --git a/kernel/modops.ml b/kernel/modops.ml
index dbd44b84a8..84c47c0032 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -114,16 +114,18 @@ let module_body_of_type mtb =
     mod_retroknowledge = []}
 
 let module_type_of_module mp mb =
-  {typ_expr = 
+  let mp1,expr = 
       (match mb.mod_type with
-	| Some expr -> expr
+	| Some expr -> mp,expr
 	| None -> (match mb.mod_expr with
-		     | Some expr -> expr
+		     | Some (SEBident mp') ->(Some mp'),(SEBident mp')
+		     | Some expr -> mp,expr
 		     | None -> 
-			 anomaly "Modops: empty expr and type"));
-   typ_alias = mb.mod_alias;
-   typ_strength = mp
-  }
+			 anomaly "Modops: empty expr and type")) in
+    {typ_expr = expr;
+      typ_alias = mb.mod_alias;
+      typ_strength = mp1
+    }
 
 let rec check_modpath_equiv env mp1 mp2 = 
   if mp1=mp2 then () else
@@ -233,19 +235,15 @@ let add_retroknowledge msid mp =
 
 
 let strengthen_const env mp l cb = 
-  match cb.const_opaque, cb.const_body with
-  | false, Some _ -> cb
-  | true, Some _ 
-  | _, None -> 
-      let const = mkConst (make_con mp empty_dirpath l) in 
-      let const_subs = Some (Declarations.from_val const) in
-	{cb with 
-      	   const_body = const_subs;
-	   const_opaque = false;
-           const_body_code = Cemitcodes.from_val
-             (compile_constant_body env const_subs false false)
-	}
-
+  let const = mkConst (make_con mp empty_dirpath l) in 
+  let const_subs = Some (Declarations.from_val const) in
+    {cb with 
+       const_body = const_subs;
+       const_opaque = false;
+       const_body_code = Cemitcodes.from_val
+        (compile_constant_body env const_subs false false)
+    }
+      
 let strengthen_mind env mp l mib = match mib.mind_equiv with
   | Some _ -> mib
   | None -> {mib with mind_equiv = Some (make_kn mp empty_dirpath l)}
@@ -330,35 +328,41 @@ and merge_with env mtb with_decl alias=
 	    Some(join (map_mp (mp_rec [id]) mp') new_alias)
 	| With_definition_body (_::_,_) 
         | With_module_body (_::_,_,_,_) -> 
-	    let old = match spec with
-		SFBmodule msb -> msb
+	    let old,aliasold = match spec with
+		SFBmodule msb -> Some msb, None
+	      | SFBalias (mpold,typ_opt,cst) ->None, Some (mpold,typ_opt,cst)
 	      | _ -> error_not_a_module (string_of_label l)
 	    in
-            let new_with_decl,subst1 = 
-	      match with_decl with
-                  With_definition_body (_,c) -> With_definition_body (idl,c),None
-		| With_module_body (idc,mp,typ_opt,cst) -> 
-		    let mp' = scrape_alias mp env' in
-		    With_module_body (idl,mp,typ_opt,cst),
-		      Some(map_mp (mp_rec (List.rev idc)) mp') 
-	    in
-	    let subst = match subst1 with
-	      | None -> None
-	      | Some s -> Some (join s (update_subst alias s)) in
-            let modtype,subst_msb = 
-              merge_with env' (type_of_mb env' old) new_with_decl alias in
-            let msb =
-	      { mod_expr = None;
-		mod_type = Some modtype; 
-		mod_constraints = old.mod_constraints;
-		mod_alias = begin 
-		  match subst_msb with
-		    |None -> empty_subst
-		    |Some s -> s
-		end;
-		mod_retroknowledge = old.mod_retroknowledge}
-	    in
-	      (SFBmodule msb),subst
+	      if aliasold = None then
+		let old = Option.get old in
+		let new_with_decl,subst1 = 
+		  match with_decl with
+                      With_definition_body (_,c) -> With_definition_body (idl,c),None
+		    | With_module_body (idc,mp,typ_opt,cst) -> 
+			let mp' = scrape_alias mp env' in
+			  With_module_body (idl,mp,typ_opt,cst),
+			Some(map_mp (mp_rec (List.rev idc)) mp') 
+		in
+		let subst = match subst1 with
+		  | None -> None
+		  | Some s -> Some (join s (update_subst alias s)) in
+		let modtype,subst_msb = 
+		  merge_with env' (type_of_mb env' old) new_with_decl alias in
+		let msb =
+		  { mod_expr = None;
+		    mod_type = Some modtype; 
+		    mod_constraints = old.mod_constraints;
+		    mod_alias = begin 
+		      match subst_msb with
+			|None -> empty_subst
+			|Some s -> s
+		    end;
+		    mod_retroknowledge = old.mod_retroknowledge}
+		in
+		  (SFBmodule msb),subst
+	      else 
+		let mpold,typ_opt,cst =  Option.get aliasold in 
+		  SFBalias (mpold,typ_opt,cst),None
       in
 	SEBstruct(msid,  before@(l,new_spec)::
 		    (Option.fold_right subst_structure subst after)),subst