Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

12 files changed, 214 insertions, 118 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 6e99bf79..f4827029 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: declarations.ml 10664 2008-03-14 11:27:37Z soubiran $ i*)
+(*i $Id: declarations.ml 11417 2008-09-17 15:06:57Z soubiran $ i*)
 
 (*i*)
 open Util
@@ -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 fa03a338..b4f5f1f7 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: declarations.mli 10664 2008-03-14 11:27:37Z soubiran $ i*)
+(*i $Id: declarations.mli 11417 2008-09-17 15:06:57Z soubiran $ i*)
 
 (*i*)
 open Names
@@ -181,7 +181,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
@@ -195,7 +196,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/indtypes.ml b/kernel/indtypes.ml
index 01b8aca1..06764834 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: indtypes.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: indtypes.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
 
 open Util
 open Names
@@ -46,6 +46,7 @@ type inductive_error =
   | SameNamesOverlap of identifier list
   | NotAnArity of identifier
   | BadEntry
+  | LargeNonPropInductiveNotInType
 
 exception InductiveError of inductive_error
 
@@ -266,7 +267,7 @@ let typecheck_inductive env mie =
       | Prop Pos when engagement env <> Some ImpredicativeSet ->
 	  (* Predicative set: check that the content is indeed predicative *)
 	  if not (is_type0m_univ lev) & not (is_type0_univ lev) then
-	    error "Large non-propositional inductive types must be in Type.";
+	    raise (InductiveError LargeNonPropInductiveNotInType);
 	  Inl (info,full_arity,s), cst
       | Prop _ ->
 	  Inl (info,full_arity,s), cst in
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 0477df82..90ae70c3 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: indtypes.mli 10425 2008-01-05 17:04:16Z herbelin $ i*)
+(*i $Id: indtypes.mli 11784 2009-01-14 11:36:32Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -33,6 +33,7 @@ type inductive_error =
   | SameNamesOverlap of identifier list
   | NotAnArity of identifier
   | BadEntry
+  | LargeNonPropInductiveNotInType
 
 exception InductiveError of inductive_error
 
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 4bb8e9d6..99ec1650 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: inductive.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: inductive.ml 11647 2008-12-02 10:40:11Z barras $ *)
 
 open Util
 open Names
@@ -683,7 +683,8 @@ let check_one_fix renv recpos def =
                     List.iter (check_rec_call renv) l
                 | Some c ->
                     try List.iter (check_rec_call renv) l
-                    with FixGuardError _ -> check_rec_call renv (applist(c,l))
+                    with FixGuardError _ ->
+                      check_rec_call renv (applist(lift p c,l))
               end
 
         | Case (ci,p,c_0,lrest) ->
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 6840febd..4a9fb606 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: mod_typing.ml 11170 2008-06-25 08:31:04Z soubiran $ i*)
+(*i $Id: mod_typing.ml 11514 2008-10-28 13:39:02Z soubiran $ i*)
 
 open Util
 open Names
@@ -37,14 +37,46 @@ 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) ->
+      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 +172,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
@@ -164,35 +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
-		    cst, (join (map_mp (mp_rec [id]) mp') up_subst)
+		  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
+		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,_ =
-			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)
+		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
-		  | 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
@@ -214,7 +259,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 +351,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 +359,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 +399,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 7bed3254..25a11c69 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modops.ml 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: modops.ml 11514 2008-10-28 13:39:02Z soubiran $ i*)
 
 (*i*)
 open Util
@@ -113,16 +113,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
@@ -132,13 +134,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 +159,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 +281,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 +307,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
@@ -314,47 +318,54 @@ and merge_with env mtb with_decl alias=
 	| [] -> MPself msid
 	| i::r -> MPdot(mp_rec r,label_of_id i)
       in 
+      let env' = add_signature (MPself msid) before env 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) ->
-	    let mp' = scrape_alias mp env in
+	| 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 (_::_,_,_) -> 
-	    let old = match spec with
-		SFBmodule msb -> msb
+        | With_module_body (_::_,_,_,_) -> 
+	    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,cst) -> 
-		    let mp' = scrape_alias mp env in
-		    With_module_body (idl,mp,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
@@ -371,7 +382,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 +413,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 +505,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 25f03495..b4dcd7c8 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: names.ml 11238 2008-07-19 09:34:03Z herbelin $ *)
+(* $Id: names.ml 11750 2009-01-05 20:47:34Z herbelin $ *)
 
 open Pp
 open Util
@@ -17,7 +17,7 @@ type identifier = string
 
 let id_ord = Pervasives.compare
 
-let id_of_string s = check_ident s; String.copy s
+let id_of_string s = check_ident_soft s; String.copy s
 
 let string_of_id id = String.copy id
 
@@ -86,6 +86,7 @@ type label = string
 
 type mod_self_id = uniq_ident
 let make_msid = make_uid
+let repr_msid (n, id, dp) = (n, id, dp)
 let debug_string_of_msid = debug_string_of_uid
 let refresh_msid (_,s,dir) = make_uid dir s
 let string_of_msid = string_of_uid
@@ -94,6 +95,7 @@ let label_of_msid (_,s,_) = s
 
 type mod_bound_id = uniq_ident
 let make_mbid = make_uid
+let repr_mbid (n, id, dp) = (n, id, dp)
 let debug_string_of_mbid = debug_string_of_uid
 let string_of_mbid = string_of_uid
 let id_of_mbid (_,s,_) = s
@@ -115,8 +117,14 @@ 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 -> string_of_dirpath sl
+  | MPfile sl -> "MPfile (" ^ string_of_dirpath sl ^ ")"
   | MPbound uid -> string_of_uid uid
   | MPself uid -> string_of_uid uid
   | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l
diff --git a/kernel/names.mli b/kernel/names.mli
index c6f59048..49b10bfe 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: names.mli 10919 2008-05-11 22:04:26Z msozeau $ i*)
+(*i $Id: names.mli 11582 2008-11-12 19:49:57Z notin $ i*)
 
 (*s Identifiers *)
 
@@ -48,6 +48,7 @@ type mod_self_id
 (* The first argument is a file name - to prevent conflict between 
    different files *)
 val make_msid : dir_path -> string -> mod_self_id
+val repr_msid : mod_self_id -> int * string * dir_path
 val id_of_msid : mod_self_id -> identifier
 val label_of_msid : mod_self_id -> label
 val refresh_msid : mod_self_id -> mod_self_id
@@ -58,6 +59,7 @@ val string_of_msid : mod_self_id -> string
 type mod_bound_id
 
 val make_mbid : dir_path -> string -> mod_bound_id
+val repr_mbid : mod_bound_id -> int * string * dir_path
 val id_of_mbid : mod_bound_id -> identifier
 val label_of_mbid : mod_bound_id -> label
 val debug_string_of_mbid : mod_bound_id -> string
@@ -82,6 +84,7 @@ 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
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 3c7461b2..fbb05a2d 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: safe_typing.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: safe_typing.ml 11453 2008-10-15 14:42:34Z soubiran $ *)
 
 open Util
 open Names
@@ -312,6 +312,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 +334,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 +509,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 +525,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;
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 14020c0b..98ee1dbb 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: subtyping.ml 11142 2008-06-18 15:37:31Z soubiran $ i*)
+(*i $Id: subtyping.ml 11453 2008-10-15 14:42:34Z soubiran $ i*)
 
 (*i*)
 open Util
@@ -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
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 11a5452c..3d254ce6 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: univ.ml 11301 2008-08-04 19:41:18Z herbelin $ *)
+(* $Id: univ.ml 11596 2008-11-16 15:34:06Z letouzey $ *)
 
 (* Initial Caml version originates from CoC 4.8 [Dec 1988] *)
 (* Extension with algebraic universes by HH [Sep 2001] *)
@@ -43,13 +43,25 @@ type universe_level =
   | Set
   | Level of Names.dir_path * int
 
+(* A specialized comparison function: we compare the [int] part first.
+   This way, most of the time, the [dir_path] part is not considered. *)
+
+let cmp_univ_level u v = match u,v with
+  | Set, Set -> 0
+  | Set, _ -> -1
+  | _, Set -> 1
+  | Level (dp1,i1), Level (dp2,i2) ->
+      if i1 < i2 then -1
+      else if i1 > i2 then 1
+      else compare dp1 dp2
+
 type universe =
   | Atom of universe_level
   | Max of universe_level list * universe_level list
   
 module UniverseOrdered = struct
   type t = universe_level
-  let compare = Pervasives.compare
+  let compare = cmp_univ_level
 end
 
 let string_of_univ_level = function
@@ -86,7 +98,8 @@ let super = function
    Used to type the products. *)
 let sup u v =
   match u,v with
-    | Atom u, Atom v -> if u = v then Atom u else Max ([u;v],[])
+    | Atom u, Atom v ->
+	if cmp_univ_level u v = 0 then Atom u else Max ([u;v],[])
     | u, Max ([],[]) -> u
     | Max ([],[]), v -> v
     | Atom u, Max (gel,gtl) -> Max (list_add_set u gel,gtl)
@@ -601,12 +614,12 @@ let dump_universes output g =
 	let u_str = string_of_univ_level u in
 	  List.iter 
 	    (fun v -> 
-	       Printf.fprintf output "%s > %s ;\n" u_str
+	       Printf.fprintf output "%s < %s ;\n" u_str
 		 (string_of_univ_level v)) 
 	    lt;
 	  List.iter 
 	    (fun v -> 
-	       Printf.fprintf output "%s >= %s ;\n" u_str
+	       Printf.fprintf output "%s <= %s ;\n" u_str
 		 (string_of_univ_level v)) 
 	    le
     | Equiv (u,v) ->