Report des commits 11417 et 11437 de la v8.2

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

8 files changed, 100 insertions, 48 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 475ef042d1..725859321c 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -251,7 +251,8 @@ type structure_field_body =
   | SFBconst of constant_body
   | SFBmind of mutual_inductive_body
   | SFBmodule of module_body
-  | SFBalias of module_path * constraints option
+  | SFBalias of module_path * struct_expr_body option 
+      * constraints option
   | SFBmodtype of module_type_body
 
 and structure_body = (label * structure_field_body) list
@@ -265,7 +266,8 @@ and struct_expr_body =
   | SEBwith of struct_expr_body * with_declaration_body
 
 and with_declaration_body =
-    With_module_body of identifier list * module_path * constraints
+    With_module_body of identifier list * module_path 
+      * struct_expr_body option  * constraints
   | With_definition_body of  identifier list * constant_body
         
 and module_body = 
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index e98cb379c2..fb8317cdcb 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -182,7 +182,8 @@ type structure_field_body =
   | SFBconst of constant_body
   | SFBmind of mutual_inductive_body
   | SFBmodule of module_body
-  | SFBalias of module_path * constraints option
+  | SFBalias of module_path * struct_expr_body option 
+      * constraints option
   | SFBmodtype of module_type_body
 
 and structure_body = (label * structure_field_body) list
@@ -196,7 +197,8 @@ and struct_expr_body =
   | SEBwith of struct_expr_body * with_declaration_body
 
 and with_declaration_body =
-    With_module_body of identifier list * module_path * constraints
+    With_module_body of identifier list * module_path 
+      * struct_expr_body option  * constraints
   | With_definition_body of  identifier list * constant_body
         
 and module_body = 
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 907b8a8fe9..941d219ba7 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -37,14 +37,41 @@ 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 type_of_struct env b meb = 
+  let rec aux env = function 
+  | SEBfunctor (mp,mtb,body) ->
+      let env = add_module (MPbound mp) (module_body_of_type mtb) env in
+	SEBfunctor(mp,mtb, aux env body)
+  | SEBident mp -> 
+      strengthen env (lookup_modtype mp env).typ_expr mp
+  | SEBapply _ as mtb -> eval_struct env mtb
+  | str -> str
+  in
+    if b then
+      Some (aux env meb)
+    else
+    None
+
+let rec bounded_str_expr = function
+     | SEBfunctor (mp,mtb,body) -> bounded_str_expr body
+     | SEBident mp -> (check_bound_mp mp)
+     | SEBapply (f,a,_)->(bounded_str_expr f)
+     | _ -> false
+
+let return_opt_type mp env mtb = 
+  if (check_bound_mp mp) then
+    Some (strengthen env mtb.typ_expr mp)
+  else
+    None
+
 let rec check_with env mtb with_decl = 
   match with_decl with
     | With_Definition (id,_) -> 
 	let cb = check_with_aux_def env mtb with_decl in
 	  SEBwith(mtb,With_definition_body(id,cb)),empty_subst
     | With_Module (id,mp) -> 
-	let cst,sub = check_with_aux_mod env mtb with_decl true in
-	  SEBwith(mtb,With_module_body(id,mp,cst)),sub
+	let cst,sub,typ_opt = check_with_aux_mod env mtb with_decl true in
+	  SEBwith(mtb,With_module_body(id,mp,typ_opt,cst)),sub
 
 and check_with_aux_def env mtb with_decl = 
   let msid,sig_b = match (eval_struct env mtb) with 
@@ -140,7 +167,7 @@ and check_with_aux_mod env mtb with_decl now =
 	  | With_Module ([id], mp) ->
 	      let old,alias = match spec with
 		  SFBmodule msb -> Some msb,None
-		| SFBalias (mp',cst) -> None,Some (mp',cst)
+		| SFBalias (mp',_,cst) -> None,Some (mp',cst)
 		| _ -> error_not_a_module (string_of_label l)
 	      in
 	      let mtb' = lookup_modtype mp env' in
@@ -165,9 +192,9 @@ and check_with_aux_mod env mtb with_decl now =
 		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
-		    cst, (join (map_mp (mp_rec [id]) mp') up_subst)
+		    cst, (join (map_mp (mp_rec [id]) mp') up_subst),(return_opt_type mp env' mtb')
 		else
-		cst,empty_subst
+		cst,empty_subst,(return_opt_type mp env' mtb')
         | With_Module (_::_,mp) -> 
 	    let old = match spec with
 		SFBmodule msb -> msb
@@ -180,7 +207,7 @@ and check_with_aux_mod env mtb with_decl now =
 			  With_Definition (_,c) -> 
 			    With_Definition (idl,c)
 			| With_Module (_,c) -> With_Module (idl,c) in
-		      let cst,_ =
+		      let cst,_,typ_opt =
 			check_with_aux_mod env' 
 			  (type_of_mb env old) new_with_decl false in
 			if now then 
@@ -188,9 +215,11 @@ and check_with_aux_mod env mtb with_decl now =
 			  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)
+			    cst, 
+		      (join (map_mp (mp_rec (List.rev (id::idl))) mp') up_subst),
+		      typ_opt
 		else
-		cst,empty_subst
+		cst,empty_subst,typ_opt
 		  | Some msb ->
                       error_a_generative_module_expected l
               end
@@ -214,7 +243,9 @@ and translate_module env me =
 	let meb,sub1 = translate_struct_entry env mexpr in
 	let mod_typ,sub,cst =
 	  match me.mod_entry_type with
-	    | None ->  None,sub1,Constraint.empty
+	    | None ->  
+		(type_of_struct env (bounded_str_expr meb) meb)
+		  ,sub1,Constraint.empty
 	    | Some mte -> 
 		let mtb2,sub2 = translate_struct_entry env mte in
                 let cst = check_subtypes env
@@ -304,7 +335,7 @@ let rec add_struct_expr_constraints env = function
   | SEBwith(meb,With_definition_body(_,cb))->
       Environ.add_constraints cb.const_constraints
 	(add_struct_expr_constraints env meb)
-  | SEBwith(meb,With_module_body(_,_,cst))->
+  | SEBwith(meb,With_module_body(_,_,_,cst))->
       Environ.add_constraints cst
 	(add_struct_expr_constraints env meb)	
 		
@@ -312,8 +343,8 @@ and add_struct_elem_constraints env = function
   | SFBconst cb -> Environ.add_constraints cb.const_constraints env
   | SFBmind mib -> Environ.add_constraints mib.mind_constraints env
   | SFBmodule mb -> add_module_constraints env mb
-  | SFBalias (mp,Some cst) -> Environ.add_constraints cst env
-  | SFBalias (mp,None) -> env
+  | SFBalias (mp,_,Some cst) -> Environ.add_constraints cst env
+  | SFBalias (mp,_,None) -> env
   | SFBmodtype mtb -> add_modtype_constraints env mtb
 
 and add_module_constraints env mb = 
@@ -352,15 +383,15 @@ let rec struct_expr_constraints cst = function
   | SEBwith(meb,With_definition_body(_,cb))->
       struct_expr_constraints
         (Univ.Constraint.union cb.const_constraints cst) meb
-  | SEBwith(meb,With_module_body(_,_,cst1))->
+  | SEBwith(meb,With_module_body(_,_,_,cst1))->
       struct_expr_constraints (Univ.Constraint.union cst1 cst) meb	
 		
 and struct_elem_constraints cst = function 
   | SFBconst cb -> cst
   | SFBmind mib -> cst
   | SFBmodule mb -> module_constraints cst mb
-  | SFBalias (mp,Some cst1) -> Univ.Constraint.union cst1 cst
-  | SFBalias (mp,None) -> cst
+  | SFBalias (mp,_,Some cst1) -> Univ.Constraint.union cst1 cst
+  | SFBalias (mp,_,None) -> cst
   | SFBmodtype mtb -> modtype_constraints cst mtb
 
 and module_constraints cst mb = 
diff --git a/kernel/modops.ml b/kernel/modops.ml
index d903d4b328..750d393cb3 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -21,6 +21,7 @@ open Mod_subst
 (*i*)
 
 
+
 let error_existing_label l = 
   error ("The label "^string_of_label l^" is already declared.")
 
@@ -132,13 +133,14 @@ let rec check_modpath_equiv env mp1 mp2 =
     else 
       error_not_equal mp1 mp2
 	
-let subst_with_body sub = function
-  | With_module_body(id,mp,cst) ->
-      With_module_body(id,subst_mp sub mp,cst)
+let rec subst_with_body sub = function
+  | With_module_body(id,mp,typ_opt,cst) ->
+      With_module_body(id,subst_mp sub mp,Option.smartmap 
+			 (subst_struct_expr sub) typ_opt,cst)
   | With_definition_body(id,cb) ->
       With_definition_body( id,subst_const_body sub cb)
 
-let rec subst_modtype sub mtb =
+and subst_modtype sub mtb =
   let typ_expr' = subst_struct_expr sub mtb.typ_expr in
     if typ_expr'==mtb.typ_expr then
       mtb
@@ -156,8 +158,9 @@ and subst_structure sub sign =
 	SFBmodule (subst_module sub mb)
     | SFBmodtype mtb -> 
 	SFBmodtype (subst_modtype sub mtb)
-    | SFBalias (mp,cst) ->
-	SFBalias (subst_mp sub mp,cst)
+    | SFBalias (mp,typ_opt,cst) ->
+	SFBalias (subst_mp sub mp,Option.smartmap 
+		    (subst_struct_expr sub) typ_opt,cst)
   in
     List.map (fun (l,b) -> (l,subst_body b)) sign
 
@@ -277,7 +280,7 @@ let rec eval_struct env = function
   | SEBwith (mtb,(With_definition_body _ as wdb)) ->
       let mtb',_ = merge_with env mtb wdb empty_subst in
 	mtb'
-  | SEBwith (mtb, (With_module_body (_,mp,_) as wdb)) ->
+  | SEBwith (mtb, (With_module_body (_,mp,_,_) as wdb)) ->
       let alias_in_mp =
 	(lookup_modtype mp env).typ_alias in
       let alias_in_mp = match eval_struct env (SEBident mp) with
@@ -303,8 +306,8 @@ and merge_with env mtb with_decl alias=
     | _ -> error_signature_expected mtb
   in
   let id,idl = match with_decl with 
-    | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_) -> id,idl
-    | With_definition_body ([],_) | With_module_body ([],_,_) -> assert false
+    | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_,_) -> id,idl
+    | With_definition_body ([],_) | With_module_body ([],_,_,_) -> assert false
   in
   let l = label_of_id id in
     try
@@ -316,16 +319,16 @@ and merge_with env mtb with_decl alias=
       in 
       let new_spec,subst = match with_decl with
         | With_definition_body ([],_)
-        | With_module_body ([],_,_) -> assert false
+        | With_module_body ([],_,_,_) -> assert false
 	| With_definition_body ([id],c) -> 
 	    SFBconst c,None
-	| With_module_body ([id], mp,cst) ->
+	| With_module_body ([id], mp,typ_opt,cst) ->
 	    let mp' = scrape_alias mp env in
 	    let new_alias = update_subst alias (map_mp (mp_rec [id]) mp') in
-	      SFBalias (mp,Some cst),
+	      SFBalias (mp,typ_opt,Some cst),
 	    Some(join (map_mp (mp_rec [id]) mp') new_alias)
 	| With_definition_body (_::_,_) 
-        | With_module_body (_::_,_,_) -> 
+        | With_module_body (_::_,_,_,_) -> 
 	    let old = match spec with
 		SFBmodule msb -> msb
 	      | _ -> error_not_a_module (string_of_label l)
@@ -333,9 +336,9 @@ and merge_with env mtb with_decl alias=
             let new_with_decl,subst1 = 
 	      match with_decl with
                   With_definition_body (_,c) -> With_definition_body (idl,c),None
-		| With_module_body (idc,mp,cst) -> 
+		| With_module_body (idc,mp,typ_opt,cst) -> 
 		    let mp' = scrape_alias mp env in
-		    With_module_body (idl,mp,cst),
+		    With_module_body (idl,mp,typ_opt,cst),
 		      Some(map_mp (mp_rec (List.rev idc)) mp') 
 	    in
 	    let subst = match subst1 with
@@ -371,7 +374,7 @@ and add_signature mp sign env =
 	| SFBmodule mb -> 
 	    add_module (MPdot (mp,l)) mb env 
 	      (* adds components as well *)
-	| SFBalias (mp1,cst) -> 
+	| SFBalias (mp1,_,cst) -> 
 	    Environ.register_alias (MPdot(mp,l)) mp1 env
 	| SFBmodtype mtb -> Environ.add_modtype (MPdot(mp,l)) 
 	    mtb env
@@ -402,7 +405,7 @@ and  constants_of_specification env mp sign =
        let new_env =  add_module (MPdot (mp,l)) mb env in 
        new_env,(constants_of_modtype env (MPdot (mp,l))
 		   (type_of_mb env mb)) @ res
-   | SFBalias (mp1,cst) ->
+   | SFBalias (mp1,typ_opt,cst) ->
        let new_env =  register_alias (MPdot (mp,l)) mp1 env in 
        new_env,(constants_of_modtype env (MPdot (mp,l))
 		   (eval_struct env (SEBident mp1))) @ res
@@ -494,7 +497,7 @@ and strengthen_sig env msid sign mp = match sign with
 	  (MPdot (MPself msid,l)) mb env in
         let rest' = strengthen_sig env' msid rest mp in
 	item':: rest'
-  | ((l,SFBalias (mp1,cst)) as item) :: rest ->
+  | ((l,SFBalias (mp1,_,cst)) as item) :: rest ->
       let env' = register_alias (MPdot(MPself msid,l)) mp1 env in
       let rest' = strengthen_sig env' msid rest mp in
 	item::rest'
diff --git a/kernel/names.ml b/kernel/names.ml
index 0191880d16..e75900cfa1 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -117,6 +117,11 @@ type module_path =
   | MPself of mod_self_id 
   | MPdot of module_path * label
 
+let rec check_bound_mp = function
+  | MPbound _ -> true
+  | MPdot(mp,_) ->check_bound_mp mp
+  | _ -> false
+
 let rec string_of_mp = function
   | MPfile sl -> "MPfile (" ^ string_of_dirpath sl ^ ")"
   | MPbound uid -> string_of_uid uid
diff --git a/kernel/names.mli b/kernel/names.mli
index 177768cf43..d0efe2380e 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -84,6 +84,8 @@ type module_path =
   | MPdot of module_path * label
 (*i  | MPapply of module_path * module_path    in the future (maybe) i*)
 
+val check_bound_mp : module_path -> bool
+
 val string_of_mp : module_path -> string
 
 module MPset : Set.S with type elt = module_path
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index eef2d675ce..09b2f918f0 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -27,6 +27,7 @@ open Subtyping
 open Mod_typing
 open Mod_subst
 
+
 type modvariant = 
   | NONE 
   | SIG of (* funsig params *) (mod_bound_id * module_type_body) list 
@@ -312,6 +313,13 @@ let add_alias l mp senv =
   check_label l senv.labset; 
   let mp' = MPdot(senv.modinfo.modpath, l) in
   let mp1 = scrape_alias mp senv.env in
+  let typ_opt = 
+    if check_bound_mp mp then
+      Some (strengthen senv.env
+	      (lookup_modtype mp senv.env).typ_expr mp)
+    else
+      None 
+  in
     (* we get all updated alias substitution {mp1.K\M}  that comes from mp1 *)
   let _,sub = Modops.update_subst senv.env (lookup_module mp1 senv.env) mp1 in
     (* transformation of {mp1.K\M} to {mp.K\M}*)
@@ -327,7 +335,7 @@ let add_alias l mp senv =
 		      alias_subst = join 
 	    senv.modinfo.alias_subst sub};
 	labset = Labset.add l senv.labset;
-	revstruct = (l,SFBalias (mp,None))::senv.revstruct;
+	revstruct = (l,SFBalias (mp,typ_opt,None))::senv.revstruct;
         univ = senv.univ;
         engagement = senv.engagement;
 	imports = senv.imports;
@@ -502,7 +510,7 @@ let end_module l restype senv =
 	       imports = senv'.imports;
 	       loads = senv'.loads;
 	       local_retroknowledge = senv'.local_retroknowledge }
-       | SFBalias (mp',cst) ->
+       | SFBalias (mp',typ_opt,cst) ->
 	   let env' = Option.fold_right 
 	     Environ.add_constraints cst senv.env in
 	   let mp = MPdot(senv.modinfo.modpath, l) in
@@ -518,7 +526,7 @@ let end_module l restype senv =
 			      alias_subst = join 
 		   senv.modinfo.alias_subst sub};
 	       labset = Labset.add l senv.labset;
-	       revstruct = (l,SFBalias (mp',cst))::senv.revstruct;
+	       revstruct = (l,SFBalias (mp',typ_opt,cst))::senv.revstruct;
                univ = senv.univ;
                engagement = senv.engagement;
 	       imports = senv.imports;
@@ -817,4 +825,3 @@ let j_type j = j.uj_type
 let safe_infer senv = infer (env_of_senv senv)
     
 let typing senv = Typeops.typing (env_of_senv senv)
-
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 918a2f51ba..387d97de97 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -33,7 +33,7 @@ type namedobject =
   | IndConstr of constructor * mutual_inductive_body
   | Module of module_body
   | Modtype of module_type_body
-  | Alias of module_path
+  | Alias of module_path * struct_expr_body option
 
 (* adds above information about one mutual inductive: all types and
    constructors *)
@@ -64,7 +64,7 @@ let make_label_map mp list =
        add_nameobjects_of_mib (make_kn mp empty_dirpath l) mib map
     | SFBmodule mb -> add_map (Module mb)
     | SFBmodtype mtb -> add_map (Modtype mtb)
-    | SFBalias (mp,cst) -> add_map (Alias mp)
+    | SFBalias (mp,typ_opt,cst) -> add_map (Alias (mp,typ_opt))
   in
     List.fold_right add_one list Labmap.empty
 
@@ -352,23 +352,23 @@ and check_signatures cst env (msid1,sig1) alias (msid2,sig2') =
 	    begin
 	      match info1 with
 		| Module msb -> check_modules cst env msid1 l msb msb2 alias
-		| Alias mp ->let msb = 
+		| Alias (mp,typ_opt) ->let msb = 
 		    {mod_expr = Some (SEBident mp);
-		     mod_type = Some (eval_struct env (SEBident mp));
+		     mod_type = typ_opt;
 		     mod_constraints = Constraint.empty;
 		     mod_alias = (lookup_modtype mp env).typ_alias;
 		     mod_retroknowledge = []} in
 		    check_modules cst env msid1 l msb msb2 alias
 		| _ -> error_not_match l spec2
 	    end
-	| SFBalias (mp,_) ->
+	| SFBalias (mp,typ_opt,_) ->
 	    begin	
 	      match info1 with
-		| Alias mp1 -> check_modpath_equiv env mp mp1; cst
+		| Alias (mp1,_) -> check_modpath_equiv env mp mp1; cst
 		| Module msb -> 
 		    let msb1 = 
 		      {mod_expr = Some (SEBident mp);
-		       mod_type = Some (eval_struct env (SEBident mp));
+		       mod_type = typ_opt;
 		       mod_constraints = Constraint.empty;
 		       mod_alias = (lookup_modtype mp env).typ_alias;
 		       mod_retroknowledge = []} in