This big commit addresses two problems:

  1- Management of the name-space in a modular development / sharing of non-logical objects.
  2- Performance of atomic module operations (adding a module to the environment, subtyping ...).

1-
There are 3 module constructions which derive equalities on fields from a module to another:
Let P be a module path and foo a field of P

Module M := P.

Module M.
 Include P.
 ...
End M.

Declare Module K : S with Module M := P.

In this 3 cases we don't want to be bothered by the duplication of names. 
Of course, M.foo delta reduce to P.foo but many non-logical features of coq 
do not work modulo conversion (they use eq_constr or constr_pat object). 
To engender a transparent name-space (ie using P.foo or M.foo is the same thing) 
we quotient the name-space by the equivalence relation on names induced by the 
3 constructions above.
To implement this, the types constant and mutual_inductive are now couples of 
kernel_names. The first projection correspond to the name used by the user and the second
projection to the canonical name, for example the internal name of M.foo is
(M.foo,P.foo). 
So:
*************************************************************************************
*  Use the eq_(con,mind,constructor,gr,egr...) function and not = on names values   *
*************************************************************************************

Map and Set indexed on names are ordered on user name for the kernel side
and on canonical name outside. Thus we have sharing of notation, hints... for free 
(also for a posteriori declaration of them, ex: a notation on M.foo will be 
avaible on P.foo). If you want to use this, use the appropriate compare function
defined in name.ml or libnames.ml.


2-
No more time explosion (i hoppe) when using modules i have re-implemented atomic
module operations so that they are all linear in the size of the module. We also
have no more unique identifier (internal module names) for modules, it is now based 
on a section_path like mechanism => we have less substitutions to perform at require,
module closing and subtyping but we pre-compute more information hence if we instanciate 
several functors then we have bigger vo.


Last thing, the checker will not work well on vo(s) that contains one of the 3 constructions
above, i will work on it soon...



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

15 files changed, 873 insertions, 851 deletions

diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 290e6ff8e..170ac6384 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -33,7 +33,7 @@ let pr_engt = function
       str "Theory: Set is predicative"
 
 let cst_filter f csts =
-  Cmap.fold
+  Cmap_env.fold
     (fun c ce acc -> if f c ce then c::acc else acc)
     csts []
 
diff --git a/checker/closure.ml b/checker/closure.ml
index b55c5848e..c710df816 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -378,7 +378,7 @@ let defined_rels flags env =
       (rel_context env) ~init:(0,[])
 (*  else (0,[])*)
 
-let mind_equiv_infos info = mind_equiv info.i_env
+let mind_equiv_infos info = eq_ind
 
 let create mk_cl flgs env =
   { i_flags = flgs;
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 0066e7848..3211cc28f 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -31,60 +31,241 @@ let val_cst_type =
 
 
 type substitution_domain =
-    MSI of mod_self_id
   | MBI of mod_bound_id
   | MPI of module_path
 
 let val_subst_dom =
-  val_sum "substitution_domain" 0 [|[|val_uid|];[|val_uid|];[|val_mp|]|]
+  val_sum "substitution_domain" 0 [|[|val_uid|];[|val_mp|]|]
 
 module Umap = Map.Make(struct
 			 type t = substitution_domain
 			 let compare = Pervasives.compare
 		       end)
 
-type resolver
 
-type substitution = (module_path * resolver option) Umap.t
+type delta_hint =
+    Inline of constr option
+  | Equiv of kernel_name
+  | Prefix_equiv of module_path
+
+type delta_key = 
+    KN of kernel_name
+  | MP of module_path
+
+module Deltamap =  Map.Make(struct 
+			      type t = delta_key
+			      let compare = Pervasives.compare
+			    end)
+
+type delta_resolver = delta_hint Deltamap.t
+
+let empty_delta_resolver = Deltamap.empty
+
+type substitution = (module_path * delta_resolver) Umap.t
 type 'a subst_fun = substitution -> 'a -> 'a
 
-let val_res = val_opt no_val
+let val_res_dom = no_val
+  (*val_sum "resolver_domain" 0 [|[|val_kn|];[|val_mp|]|]*)
+
+let val_res = no_val
+ (* val_map ~name:"delta_resolver"
+    val_res_dom  
+    (val_sum "resolver_codomain" 0 [|[|val_opt val_constr||];[|val_kn|];[|val_mp|]|])*)
 
 let val_subst =
   val_map ~name:"substitution"
     val_subst_dom (val_tuple "substition range" [|val_mp;val_res|])
 
 
-let fold_subst fs fb fp =
+let fold_subst fb fp =
   Umap.fold
     (fun k (mp,_) acc ->
       match k with
-          MSI msid -> fs msid mp acc
         | MBI mbid -> fb mbid mp acc
         | MPI mp1 -> fp mp1 mp acc)
 
 let empty_subst = Umap.empty
 
-let add_msid msid mp =
-  Umap.add (MSI msid) (mp,None)
 let add_mbid mbid mp =
-  Umap.add (MBI mbid) (mp,None)
+  Umap.add (MBI mbid) (mp,empty_delta_resolver)
 let add_mp mp1 mp2  =
-  Umap.add (MPI mp1) (mp2,None)
+  Umap.add (MPI mp1) (mp2,empty_delta_resolver)
 
-let map_msid msid mp = add_msid msid mp empty_subst
 let map_mbid mbid mp = add_mbid mbid mp empty_subst
 let map_mp mp1 mp2 = add_mp mp1 mp2 empty_subst
 
+let add_inline_delta_resolver con =
+  Deltamap.add (KN(user_con con)) (Inline None)
+    
+let add_inline_constr_delta_resolver con cstr =
+  Deltamap.add (KN(user_con con)) (Inline (Some cstr))
+
+let add_constant_delta_resolver con =
+  Deltamap.add (KN(user_con con)) (Equiv (canonical_con con))
+
+let add_mind_delta_resolver mind =
+  Deltamap.add (KN(user_mind mind)) (Equiv (canonical_mind mind))
+
+let add_mp_delta_resolver mp1 mp2 = 
+  Deltamap.add (MP mp1) (Prefix_equiv mp2)
+
+let mp_in_delta mp = 
+  Deltamap.mem (MP mp) 
+
+let con_in_delta con resolver = 
+try 
+  match Deltamap.find (KN(user_con con)) resolver with
+  | Inline _  | Prefix_equiv _ -> false
+  | Equiv _ -> true
+with
+ Not_found -> false
+
+let mind_in_delta mind resolver = 
+try 
+  match Deltamap.find (KN(user_mind mind)) resolver with
+  | Inline _  | Prefix_equiv _ -> false
+  | Equiv _ -> true
+with
+ Not_found -> false
+
+let delta_of_mp resolve mp =
+  try 
+    match Deltamap.find (MP mp) resolve with
+      | Prefix_equiv mp1 -> mp1
+      | _ -> anomaly "mod_subst: bad association in delta_resolver"
+  with
+      Not_found -> mp
+	
+let delta_of_kn resolve kn =
+  try 
+    match Deltamap.find (KN kn) resolve with
+      | Equiv kn1 -> kn1
+      | Inline _ -> kn
+      | _ -> anomaly 
+	  "mod_subst: bad association in delta_resolver"
+  with
+      Not_found -> kn
+
+let remove_mp_delta_resolver resolver mp =
+    Deltamap.remove (MP mp) resolver
+
+exception Inline_kn
+
+let rec find_prefix resolve mp = 
+  let rec sub_mp = function
+    | MPdot(mp,l) as mp_sup -> 
+	(try 
+	   match Deltamap.find (MP mp_sup) resolve with
+	     | Prefix_equiv mp1 -> mp1
+	     | _ -> anomaly 
+		 "mod_subst: bad association in delta_resolver"
+	 with
+	     Not_found -> MPdot(sub_mp mp,l))
+    | p -> 
+	match Deltamap.find (MP p) resolve with
+	  | Prefix_equiv mp1 -> mp1
+	  | _ -> anomaly 
+		 "mod_subst: bad association in delta_resolver"	
+  in
+    try 
+      sub_mp mp
+    with
+	Not_found -> mp
+	  
+let solve_delta_kn resolve kn =
+  try 
+      match Deltamap.find (KN kn) resolve with
+	| Equiv kn1 -> kn1
+	| Inline _ -> raise Inline_kn
+	| _ -> anomaly 
+	    "mod_subst: bad association in delta_resolver"
+  with
+      Not_found | Inline_kn -> 
+	let mp,dir,l = repr_kn kn in
+	let new_mp = find_prefix resolve mp in
+	  if mp == new_mp then 
+	    kn
+	  else
+	    make_kn new_mp dir l
+	      
+
+let constant_of_delta resolve con =
+  let kn = user_con con in
+  let new_kn = solve_delta_kn resolve kn in
+    if kn == new_kn then
+      con
+    else
+      constant_of_kn_equiv kn new_kn
+	
+let constant_of_delta2 resolve con =
+  let kn = canonical_con con in
+  let kn1 = user_con con in
+  let new_kn = solve_delta_kn resolve kn in
+    if kn == new_kn then
+      con
+    else
+      constant_of_kn_equiv kn1 new_kn
+
+let mind_of_delta resolve mind =
+  let kn = user_mind mind in
+  let new_kn = solve_delta_kn resolve kn in
+    if kn == new_kn then
+      mind
+    else
+      mind_of_kn_equiv kn new_kn
+	
+let mind_of_delta2 resolve mind =
+  let kn = canonical_mind mind in
+  let kn1 = user_mind mind in
+  let new_kn = solve_delta_kn resolve kn in
+    if kn == new_kn then
+      mind
+    else
+      mind_of_kn_equiv kn1 new_kn
+
+
+
+let inline_of_delta resolver = 
+  let extract key hint l =
+    match key,hint with 
+      |KN kn, Inline _ -> kn::l
+      | _,_ -> l
+  in
+    Deltamap.fold extract resolver []
+
+exception Not_inline
+  
+let constant_of_delta_with_inline resolve con =
+  let kn1,kn2 = canonical_con con,user_con con in
+    try
+      match Deltamap.find (KN kn2) resolve with 
+	| Inline None -> None
+	| Inline (Some const) -> Some const
+	| _ -> raise Not_inline
+    with
+	Not_found | Not_inline -> 
+	  try match Deltamap.find (KN kn1) resolve with 
+	    | Inline None -> None
+	    | Inline (Some const) -> Some const
+	    | _ -> raise Not_inline
+	  with
+	      Not_found | Not_inline -> None
+
 let subst_mp0 sub mp = (* 's like subst *)
  let rec aux mp =
   match mp with
-    | MPself sid ->
-        let mp',resolve = Umap.find (MSI sid) sub in
+    | MPfile sid -> 
+        let mp',resolve = Umap.find (MPI (MPfile sid)) sub in
          mp',resolve
     | MPbound bid ->
-        let mp',resolve = Umap.find (MBI bid) sub in
-          mp',resolve
+	begin
+	  try
+            let mp',resolve = Umap.find (MBI bid) sub in
+              mp',resolve
+	  with Not_found ->
+	    let mp',resolve = Umap.find (MPI mp) sub in
+              mp',resolve
+	end
     | MPdot (mp1,l) as mp2 ->
 	begin
 	  try
@@ -94,59 +275,135 @@ let subst_mp0 sub mp = (* 's like subst *)
 	    let mp1',resolve = aux mp1 in
 	      MPdot (mp1',l),resolve
 	end
-    | _ -> raise Not_found
  in
   try
     Some (aux mp)
   with Not_found -> None
 
-
-
-let subst_mp0 sub mp = (* 's like subst *)
- let rec aux mp =
-  match mp with
-    | MPself sid -> fst (Umap.find (MSI sid) sub)
-    | MPbound bid -> fst (Umap.find (MBI bid) sub)
-    | MPdot (mp1,l) as mp2 ->
-	begin
-	  try fst (Umap.find (MPI mp2) sub)
-	  with Not_found -> MPdot (aux mp1,l)
-	end
-
-    | _ -> raise Not_found
- in
-  try Some (aux mp) with Not_found -> None
-
 let subst_mp sub mp =
  match subst_mp0 sub mp with
     None -> mp
-  | Some mp' -> mp'
+  | Some (mp',_) -> mp'
 
-let subst_kn0 sub kn =
+let subst_kn_delta sub kn =
  let mp,dir,l = repr_kn kn in
   match subst_mp0 sub mp with
-     Some mp' ->
-      Some (make_kn mp' dir l)
-   | None -> None
+     Some (mp',resolve) ->
+      solve_delta_kn resolve (make_kn mp' dir l)
+   | None -> kn
 
 let subst_kn sub kn =
- match subst_kn0 sub kn with
-    None -> kn
-  | Some kn' -> kn'
+ let mp,dir,l = repr_kn kn in
+  match subst_mp0 sub mp with
+     Some (mp',_) ->
+      make_kn mp' dir l
+   | None -> kn
+
+exception No_subst
+
+type sideconstantsubst =
+  | User
+  | Canonical
+
+let subst_ind sub mind =
+  let kn1,kn2 = user_mind mind,canonical_mind mind in
+  let mp1,dir,l = repr_kn kn1 in
+  let mp2,_,_ = repr_kn kn2 in
+    try 
+      let side,mind',resolve =   
+        match subst_mp0 sub mp1,subst_mp0 sub mp2 with
+	    None,None ->raise No_subst
+	  | Some (mp',resolve),None -> User,(make_mind_equiv mp' mp2 dir l), resolve
+	  | None, Some(mp',resolve)-> Canonical,(make_mind_equiv mp1 mp' dir l), resolve
+	  | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical,
+	      (make_mind_equiv mp1' mp2' dir l), resolve2 
+      in
+	match side with
+	  |User ->
+	     let mind = mind_of_delta resolve mind' in
+	       mind
+	  |Canonical ->
+	     let mind = mind_of_delta2 resolve mind' in
+	       mind
+    with 
+	No_subst -> mind
+
+let subst_mind0 sub mind =
+  let kn1,kn2 = user_mind mind,canonical_mind mind in
+  let mp1,dir,l = repr_kn kn1 in
+  let mp2,_,_ = repr_kn kn2 in
+    try 
+      let side,mind',resolve =   
+        match subst_mp0 sub mp1,subst_mp0 sub mp2 with
+	    None,None ->raise No_subst
+	  | Some (mp',resolve),None -> User,(make_mind_equiv mp' mp2 dir l), resolve
+	  | None, Some(mp',resolve)-> Canonical,(make_mind_equiv mp1 mp' dir l), resolve
+	  | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical,
+	      (make_mind_equiv mp1' mp2' dir l), resolve2
+      in
+	match side with
+	  |User ->
+	     let mind = mind_of_delta resolve mind' in
+	       Some mind
+	  |Canonical ->
+	     let mind = mind_of_delta2 resolve mind' in
+	       Some mind
+    with 
+	No_subst -> Some mind
 
 let subst_con sub con =
- let mp,dir,l = repr_con con in
-  match subst_mp0 sub mp with
-     None -> con
-   | Some mp' -> make_con mp' dir l
+  let kn1,kn2 = user_con con,canonical_con con in
+  let mp1,dir,l = repr_kn kn1 in
+  let mp2,_,_ = repr_kn kn2 in
+    try 
+      let side,con',resolve =   
+        match subst_mp0 sub mp1,subst_mp0 sub mp2 with
+	    None,None ->raise No_subst
+	  | Some (mp',resolve),None -> User,(make_con_equiv mp' mp2 dir l), resolve
+	  | None, Some(mp',resolve)-> Canonical,(make_con_equiv mp1 mp' dir l), resolve
+	  | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical,
+	      (make_con_equiv mp1' mp2' dir l), resolve2 
+      in
+	match constant_of_delta_with_inline resolve con' with
+            None -> begin
+	      match side with
+	      |User ->
+	      let con = constant_of_delta resolve con' in
+		con,Const con
+	      |Canonical ->
+		  let con = constant_of_delta2 resolve con' in
+		con,Const con
+	    end
+	  | Some t -> con',t
+    with No_subst -> con , Const con 
+ 
 
 let subst_con0 sub con =
- let mp,dir,l = repr_con con in
-  match subst_mp0 sub mp with
-      None -> None
-    | Some mp' ->
-	let con' = make_con mp' dir l in
-        Some (Const con')
+  let kn1,kn2 = user_con con,canonical_con con in
+  let mp1,dir,l = repr_kn kn1 in
+  let mp2,_,_ = repr_kn kn2 in
+    try  
+      let side,con',resolve =   
+	match subst_mp0 sub mp1,subst_mp0 sub mp2 with
+	    None,None ->raise No_subst
+	  | Some (mp',resolve),None -> User,(make_con_equiv mp' mp2 dir l), resolve
+	  | None, Some(mp',resolve)-> Canonical,(make_con_equiv mp1 mp' dir l), resolve
+	  | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical,
+	      (make_con_equiv mp1' mp2' dir l), resolve2 
+      in
+	match constant_of_delta_with_inline resolve con' with
+	    None ->begin
+	      match side with
+	      |User ->
+	      let con = constant_of_delta resolve con' in
+		Some (Const con)
+	      |Canonical ->
+		  let con = constant_of_delta2 resolve con' in
+		Some (Const con)
+	    end
+	  | t ->  t
+    with No_subst -> Some (Const con)
+
 
 let rec map_kn f f' c =
   let func = map_kn f f' in
@@ -220,22 +477,8 @@ let rec map_kn f f' c =
       | _ -> c
 
 let subst_mps sub =
-  map_kn (subst_kn0 sub) (subst_con0 sub)
+  map_kn (subst_mind0 sub) (subst_con0 sub)
 
-let rec replace_mp_in_mp mpfrom mpto mp =
-  match mp with
-    | _ when mp = mpfrom -> mpto
-    | MPdot (mp1,l) ->
-	let mp1' = replace_mp_in_mp mpfrom mpto mp1 in
-	  if mp1==mp1' then mp
-	  else MPdot (mp1',l)
-    | _ -> mp
-
-let replace_mp_in_con mpfrom mpto kn =
- let mp,dir,l = kn in
-  let mp'' = replace_mp_in_mp mpfrom mpto mp in
-    if mp==mp'' then kn
-    else (mp'', dir, l)
 
 type 'a lazy_subst =
   | LSval of 'a
@@ -253,117 +496,115 @@ let force fsubst r =
       r := LSval a';
       a'
 
-
-
-let join (subst1 : substitution) (subst2 : substitution) =
-  let apply_subst (sub : substitution) key (mp,_) =
-      match subst_mp0 sub mp with
-	  None -> mp,None
-	| Some mp' -> mp',None in
-  let subst = Umap.mapi (apply_subst subst2) subst1 in
-    (Umap.fold Umap.add subst2 subst)
-
-let subst_key subst1 subst2 =
-  let replace_in_key key mp sub=
-    let newkey =
-      match key with
-	| MPI mp1 ->
-	    begin
-	      match subst_mp0 subst1 mp1 with
-		| None -> None
-		| Some mp2 -> Some (MPI mp2)
-	    end
-	| _ -> None
-    in
-      match newkey with
-	| None -> Umap.add key mp sub
-	| Some mpi -> Umap.add mpi mp sub
+let mp_in_key mp key = 
+  let rec mp_rec mp1 = 
+    match mp1 with
+      | _ when mp1 = mp -> true
+      | MPdot (mp2,l) -> mp_rec mp2
+      | _ -> false
+  in 
+    match key with
+    | MP mp1 -> 
+	mp_rec mp1
+    | KN kn -> 
+	let mp1,dir,l = repr_kn kn in
+	  mp_rec mp1
+   
+let subset_prefixed_by mp resolver =
+  let prefixmp key hint resolv =
+    if mp_in_key mp key then
+      Deltamap.add key hint resolv
+    else 
+      resolv
   in
-    Umap.fold replace_in_key subst2 empty_subst
-
-let update_subst_alias subst1 subst2 =
- let subst_inv key (mp,_) sub =
-    let newmp =
-      match key with
-	| MBI msid -> Some (MPbound msid)
-	| MSI msid -> Some (MPself msid)
-	| _ -> None
-    in
-      match newmp with
-	| None -> sub
-	| Some mpi -> match mp with
-	    | MPbound mbid -> Umap.add (MBI mbid) (mpi,None) sub
-	    | MPself msid -> Umap.add (MSI msid) (mpi,None) sub
-	    | _ ->  Umap.add (MPI mp) (mpi,None) sub
+    Deltamap.fold prefixmp resolver empty_delta_resolver
+
+let subst_dom_delta_resolver subst resolver =
+  let apply_subst key hint resolver =
+    match key with
+	(MP mp) ->
+	  Deltamap.add (MP (subst_mp subst mp)) hint resolver
+      | (KN kn) ->
+	  Deltamap.add (KN (subst_kn subst kn)) hint resolver
   in
-  let subst_mbi = Umap.fold subst_inv subst2 empty_subst in
-  let alias_subst key (mp,_) sub=
-    let newkey =
-      match key with
-	| MPI mp1 ->
-	    begin
-	      match subst_mp0 subst_mbi mp1 with
-		| None -> None
-		| Some mp2 -> Some (MPI mp2)
-	    end
-	| _ -> None
-    in
-      match newkey with
-	| None -> Umap.add key (mp,None) sub
-	| Some mpi -> Umap.add mpi (mp,None) sub
-  in
-    Umap.fold alias_subst subst1 empty_subst
+    Deltamap.fold apply_subst resolver empty_delta_resolver
 
-let join_alias (subst1 : substitution) (subst2 : substitution) =
-  let apply_subst (sub : substitution) key (mp,_) =
-      match subst_mp0 sub mp with
-	  None -> mp,None
-	| Some mp' -> mp',None in
-  Umap.mapi (apply_subst subst2) subst1
-
-
-let update_subst subst1 subst2 =
- let subst_inv key (mp,_) l =
-    let newmp =
-      match key with
-	| MBI msid -> MPbound msid
-	| MSI msid -> MPself msid
-	| MPI mp -> mp
-    in
-   match mp with
-     | MPbound mbid ->  ((MBI mbid),newmp)::l
-     | MPself msid ->  ((MSI msid),newmp)::l
-     | _ ->   ((MPI mp),newmp)::l
+let subst_mp_delta sub mp key=
+ match subst_mp0 sub mp with
+    None -> empty_delta_resolver,mp
+  | Some (mp',resolve) -> 
+      let mp1 = find_prefix resolve mp' in
+      let resolve1 = subset_prefixed_by mp1 resolve in
+	match key with
+	    MP mpk ->
+	      (subst_dom_delta_resolver 
+		 (map_mp mp1 mpk) resolve1),mp1
+	  | _ -> anomaly "Mod_subst: Bad association in resolver" 
+
+let subst_codom_delta_resolver subst resolver =
+  let apply_subst key hint resolver =
+    match hint with
+	Prefix_equiv mp ->
+	  let derived_resolve,mpnew = subst_mp_delta subst mp key in
+	    Deltamap.fold Deltamap.add derived_resolve
+	      (Deltamap.add key (Prefix_equiv mpnew) resolver)
+      | (Equiv kn) ->
+	  Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver
+      | Inline None ->
+	  Deltamap.add key hint resolver
+      | Inline (Some t) ->
+	  Deltamap.add key (Inline (Some (subst_mps subst t))) resolver
   in
-  let subst_mbi = Umap.fold subst_inv subst2 [] in
-  let alias_subst key (mp,_) sub=
-    let newsetkey =
-      match key with
-	| MPI mp1 ->
-	    let compute_set_newkey l (k,mp') =
-	      let mp_from_key = match k with
-		  	| MBI msid -> MPbound msid
-			| MSI msid -> MPself msid
-			| MPI mp -> mp
-	      in
-	      let new_mp1 = replace_mp_in_mp mp_from_key mp' mp1 in
-		if new_mp1 == mp1 then l else (MPI new_mp1)::l
-	    in
-	    begin
-	      match List.fold_left compute_set_newkey [] subst_mbi with
-		| [] -> None
-		| l -> Some (l)
-	    end
-	| _ -> None
+    Deltamap.fold apply_subst resolver empty_delta_resolver
+
+let subst_dom_codom_delta_resolver subst resolver =
+  subst_dom_delta_resolver subst
+    (subst_codom_delta_resolver subst resolver)
+    
+let update_delta_resolver resolver1 resolver2 =
+ let apply_res key hint res = 
+      try
+	match hint with
+	    Prefix_equiv mp ->
+	      let new_hint =
+		Prefix_equiv (find_prefix resolver2 mp)
+	      in Deltamap.add key new_hint res
+	  | Equiv kn ->
+	      let new_hint =
+		Equiv (solve_delta_kn resolver2 kn)
+	      in Deltamap.add key new_hint res
+	  | _ -> Deltamap.add key hint res
+      with not_found -> 
+	Deltamap.add key hint res
     in
-      match newsetkey with
-	| None -> sub
-	| Some l ->
-	    List.fold_left (fun s k -> Umap.add k (mp,None) s)
-	      sub l
-  in
-    Umap.fold alias_subst subst1 empty_subst
+      Deltamap.fold apply_res resolver1 empty_delta_resolver
+
+let add_delta_resolver resolver1 resolver2 =
+  if resolver1 == resolver2 then
+    resolver2
+  else
+    Deltamap.fold Deltamap.add (update_delta_resolver resolver1 resolver2)
+      resolver2
 
+let join (subst1 : substitution) (subst2 : substitution) =
+  let apply_subst (sub : substitution) key (mp,resolve) =
+    let mp',resolve' =
+      match subst_mp0 sub mp with
+	  None -> mp, None
+	| Some (mp',resolve') ->  mp'
+	    ,Some resolve' in
+    let resolve'' : delta_resolver =
+      match resolve' with
+          Some res -> 
+	    add_delta_resolver 
+	      (subst_dom_codom_delta_resolver sub resolve)
+	      res
+	| None -> 
+	    subst_codom_delta_resolver sub resolve
+    in
+      mp',resolve'' in
+  let subst = Umap.mapi (apply_subst subst2) subst1 in
+    (Umap.fold Umap.add subst2 subst)   
 
 let subst_substituted s r =
   match !r with
@@ -414,7 +655,7 @@ let val_recarg = val_sum "recarg" 1 (* Norec *)
 
 let subst_recarg sub r = match r with
   | Norec | Mrec _  -> r
-  | Imbr (kn,i) -> let kn' = subst_kn sub kn in
+  | Imbr (kn,i) -> let kn' = subst_ind sub kn in
       if kn==kn' then r else Imbr (kn',i)
 
 type wf_paths = recarg Rtree.t
@@ -547,8 +788,6 @@ type mutual_inductive_body = {
   (* Universes constraints enforced by the inductive declaration *)
     mind_constraints : Univ.constraints;
 
-  (* Source of the inductive block when aliased in a module *)
-    mind_equiv : kernel_name option
   }
 let val_ind_pack = val_tuple "mutual_inductive_body"
   [|val_array val_one_ind;val_bool;val_bool;val_int;val_nctxt;
@@ -605,8 +844,7 @@ let subst_mind sub mib =
     mind_params_ctxt =
       map_rel_context (subst_mps sub) mib.mind_params_ctxt;
     mind_packets = array_smartmap (subst_mind_packet sub) mib.mind_packets ;
-    mind_constraints = mib.mind_constraints ;
-    mind_equiv = Option.map (subst_kn sub) mib.mind_equiv }
+    mind_constraints = mib.mind_constraints  }
 
 (* Modules *)
 
@@ -616,7 +854,6 @@ type structure_field_body =
   | SFBconst of constant_body
   | SFBmind of mutual_inductive_body
   | SFBmodule of module_body
-  | SFBalias of module_path * struct_expr_body option * Univ.constraints option
   | SFBmodtype of module_type_body
 
 and structure_body = (label * structure_field_body) list
@@ -624,116 +861,120 @@ and structure_body = (label * structure_field_body) list
 and struct_expr_body =
   | SEBident of module_path
   | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body
-  | SEBstruct of mod_self_id * structure_body
-  | SEBapply of struct_expr_body * struct_expr_body
-      * Univ.constraints
+  | SEBapply of struct_expr_body * struct_expr_body * Univ.constraints
+  | SEBstruct of structure_body
   | SEBwith of struct_expr_body * with_declaration_body
 
 and with_declaration_body =
-    With_module_body of identifier list * module_path *
-      struct_expr_body option * Univ.constraints
+    With_module_body of identifier list * module_path
   | With_definition_body of  identifier list * constant_body
 
 and module_body =
-    { mod_expr : struct_expr_body option;
-      mod_type : struct_expr_body option;
+    { mod_mp : module_path;
+      mod_expr : struct_expr_body option; 
+      mod_type : struct_expr_body;
+      mod_type_alg : struct_expr_body option;
       mod_constraints : Univ.constraints;
-      mod_alias : substitution;
+      mod_delta : delta_resolver;
       mod_retroknowledge : action list}
 
 and module_type_body =
-    { typ_expr : struct_expr_body;
-      typ_strength : module_path option;
-      typ_alias : substitution}
+    { typ_mp : module_path;
+      typ_expr : struct_expr_body;
+      typ_expr_alg : struct_expr_body option ;
+      typ_constraints : Univ.constraints;
+      typ_delta :delta_resolver}
 
 (* the validation functions: *)
 let rec val_sfb o = val_sum "struct_field_body" 0
   [|[|val_cb|];       (* SFBconst *)
     [|val_ind_pack|]; (* SFBmind *)
     [|val_module|];   (* SFBmodule *)
-    [|val_mp;val_opt val_seb;val_opt val_cstrs|]; (* SFBalias *)
     [|val_modtype|]   (* SFBmodtype *)
   |] o
 and val_sb o = val_list (val_tuple"label*sfb"[|val_id;val_sfb|]) o
 and val_seb o = val_sum "struct_expr_body" 0
   [|[|val_mp|];                      (* SEBident *)
     [|val_uid;val_modtype;val_seb|]; (* SEBfunctor *)
-    [|val_uid;val_sb|];              (* SEBstruct *)
+    [|val_sb|];              (* SEBstruct *)
     [|val_seb;val_seb;val_cstrs|];   (* SEBapply *)
     [|val_seb;val_with|]             (* SEBwith *)
   |] o
 and val_with o = val_sum "with_declaration_body" 0
-  [|[|val_list val_id;val_mp;val_cstrs|];
+  [|[|val_list val_id;val_mp|];
     [|val_list val_id;val_cb|]|] o
 and val_module o = val_tuple "module_body"
-  [|val_opt val_seb;val_opt val_seb;val_cstrs;val_subst;no_val|] o
+  [|val_mp;val_opt val_seb;val_opt val_seb;
+    val_seb;val_cstrs;val_res;no_val|] o
 and val_modtype o = val_tuple "module_type_body"
-  [|val_seb;val_opt val_mp;val_subst|] o
+  [|val_mp;val_seb;val_opt val_seb;val_cstrs;val_res|] o
 
 
 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_module_body(id,mp) ->
+      With_module_body(id,subst_mp sub mp)
   | With_definition_body(id,cb) ->
       With_definition_body( id,subst_const_body sub cb)
 
-and 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
+  let typ_alg' = 
+    Option.smartmap 
+      (subst_struct_expr sub) mtb.typ_expr_alg in
+  let mp = subst_mp sub mtb.typ_mp
+  in
+    if typ_expr'==mtb.typ_expr && 
+      typ_alg'==mtb.typ_expr_alg && mp==mtb.typ_mp then
+	mtb
     else
-      { mtb with
-	  typ_expr = typ_expr'}
-
-and subst_structure sub sign =
-  let subst_body  = function
-      SFBconst cb ->
+      {mtb with 
+	 typ_mp = mp;
+	 typ_expr = typ_expr';
+	 typ_expr_alg = typ_alg'}
+
+and subst_structure sub sign = 
+  let subst_body = function
+      SFBconst cb -> 
 	SFBconst (subst_const_body sub cb)
-    | SFBmind mib ->
+    | SFBmind mib -> 
 	SFBmind (subst_mind sub mib)
-    | SFBmodule mb ->
-	SFBmodule (subst_module sub mb)
-    | SFBmodtype mtb ->
+    | SFBmodule mb -> 
+	SFBmodule (subst_module sub  mb)
+    | SFBmodtype mtb -> 
 	SFBmodtype (subst_modtype sub mtb)
- | 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
 
-and subst_module  sub mb =
-  let mtb' = Option.smartmap (subst_struct_expr sub) mb.mod_type in
-  (* This is similar to the previous case. In this case we have
-     a module M in a signature that is knows to be equivalent to a module M'
-     (because the signature is "K with Module M := M'") and we are substituting
-     M' with some M''. *)
-  let me' = Option.smartmap (subst_struct_expr sub) mb.mod_expr in
-  let mb_alias = join_alias mb.mod_alias sub in
-    if mtb'==mb.mod_type && mb.mod_expr == me'
-      && mb_alias == mb.mod_alias
-    then mb else
-      { mod_expr = me';
-	mod_type=mtb';
-	mod_constraints=mb.mod_constraints;
-	mod_alias = mb_alias;
-	mod_retroknowledge=mb.mod_retroknowledge}
 
+and subst_module sub mb =
+  let mtb' = subst_struct_expr sub mb.mod_type in
+  let typ_alg' = Option.smartmap 
+    (subst_struct_expr sub ) mb.mod_type_alg in
+  let me' = Option.smartmap 
+    (subst_struct_expr sub) mb.mod_expr in
+  let mp = subst_mp sub mb.mod_mp in
+     if mtb'==mb.mod_type && mb.mod_expr == me' 
+       && mp == mb.mod_mp
+    then mb else
+      { mb with
+	  mod_mp = mp;
+	  mod_expr = me';
+	  mod_type_alg = typ_alg';
+	  mod_type=mtb'}
 
 and subst_struct_expr sub = function
-    | SEBident mp -> SEBident (subst_mp sub  mp)
-    | SEBfunctor (msid, mtb, meb') ->
-	SEBfunctor(msid,subst_modtype sub mtb,subst_struct_expr sub meb')
-    | SEBstruct (msid,str)->
-	SEBstruct(msid, subst_structure sub str)
+    | SEBident mp -> SEBident (subst_mp sub mp)
+    | SEBfunctor (mbid, mtb, meb') -> 
+	SEBfunctor(mbid,subst_modtype sub mtb
+		     ,subst_struct_expr sub meb')
+    | SEBstruct (str)->
+	SEBstruct( subst_structure sub  str)
     | SEBapply (meb1,meb2,cst)->
 	SEBapply(subst_struct_expr sub meb1,
 		 subst_struct_expr sub meb2,
 		 cst)
-    | SEBwith (meb,wdb)->
+    | SEBwith (meb,wdb)-> 
 	SEBwith(subst_struct_expr sub meb,
 		subst_with_body sub wdb)
 
 
-let subst_signature_msid msid mp =
-  subst_structure (map_msid msid mp)
diff --git a/checker/declarations.mli b/checker/declarations.mli
index 3d061b4c2..bae7da908 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -141,19 +141,18 @@ type mutual_inductive_body = {
   (* Universes constraints enforced by the inductive declaration *)
     mind_constraints : Univ.constraints;
 
-  (* Source of the inductive block when aliased in a module *)
-    mind_equiv : kernel_name option
   }
 
 (* Modules *)
 
 type substitution
+type delta_resolver
+val empty_delta_resolver : delta_resolver
 
 type structure_field_body =
   | SFBconst of constant_body
   | SFBmind of mutual_inductive_body
   | SFBmodule of module_body
-  | SFBalias of module_path * struct_expr_body option * Univ.constraints option
   | SFBmodtype of module_type_body
 
 and structure_body = (label * structure_field_body) list
@@ -161,32 +160,33 @@ and structure_body = (label * structure_field_body) list
 and struct_expr_body =
   | SEBident of module_path
   | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body
-  | SEBstruct of mod_self_id * structure_body
-  | SEBapply of struct_expr_body * struct_expr_body
-      * Univ.constraints
+  | SEBapply of struct_expr_body * struct_expr_body * Univ.constraints
+  | SEBstruct of structure_body
   | SEBwith of struct_expr_body * with_declaration_body
 
 and with_declaration_body =
-    With_module_body of identifier list * module_path *
-      struct_expr_body option * Univ.constraints
+    With_module_body of identifier list * module_path
   | With_definition_body of  identifier list * constant_body
 
 and module_body =
-    { mod_expr : struct_expr_body option;
-      mod_type : struct_expr_body option;
+    { mod_mp : module_path;
+      mod_expr : struct_expr_body option; 
+      mod_type : struct_expr_body;
+      mod_type_alg : struct_expr_body option;
       mod_constraints : Univ.constraints;
-      mod_alias : substitution;
+      mod_delta : delta_resolver;
       mod_retroknowledge : action list}
 
 and module_type_body =
-    { typ_expr : struct_expr_body;
-      typ_strength : module_path option;
-      typ_alias : substitution}
+    { typ_mp : module_path;
+      typ_expr : struct_expr_body;
+      typ_expr_alg : struct_expr_body option ;
+      typ_constraints : Univ.constraints;
+      typ_delta :delta_resolver}
 
 (* Substitutions *)
 
 val fold_subst :
-  (mod_self_id -> module_path -> 'a -> 'a) ->
   (mod_bound_id -> module_path -> 'a -> 'a) ->
   (module_path -> module_path -> 'a -> 'a) ->
   substitution -> 'a -> 'a
@@ -194,10 +194,8 @@ val fold_subst :
 type 'a subst_fun = substitution -> 'a -> 'a
 
 val empty_subst : substitution
-val add_msid : mod_self_id -> module_path -> substitution -> substitution
 val add_mbid : mod_bound_id -> module_path -> substitution -> substitution
 val add_mp   : module_path -> module_path -> substitution -> substitution
-val map_msid : mod_self_id -> module_path -> substitution
 val map_mbid : mod_bound_id -> module_path -> substitution
 val map_mp   : module_path -> module_path -> substitution
 
@@ -206,14 +204,9 @@ val subst_mind : mutual_inductive_body subst_fun
 val subst_modtype : substitution -> module_type_body -> module_type_body
 val subst_struct_expr :  substitution -> struct_expr_body -> struct_expr_body
 val subst_structure : substitution -> structure_body -> structure_body
-val subst_signature_msid :
-  mod_self_id -> module_path -> structure_body -> structure_body
+val subst_module : substitution -> module_body -> module_body
 
 val join : substitution -> substitution -> substitution
-val join_alias : substitution -> substitution -> substitution
-val update_subst_alias : substitution -> substitution -> substitution
-val update_subst : substitution -> substitution -> substitution
-val subst_key : substitution -> substitution -> substitution
 
 (* Validation *)
 val val_eng : Obj.t -> unit
diff --git a/checker/environ.ml b/checker/environ.ml
index 2d5ff3e43..3d14b995b 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -5,11 +5,10 @@ open Term
 open Declarations
 
 type globals = {
-  env_constants : constant_body Cmap.t;
-  env_inductives : mutual_inductive_body KNmap.t;
+  env_constants : constant_body Cmap_env.t;
+  env_inductives : mutual_inductive_body Mindmap_env.t;
   env_modules : module_body MPmap.t;
-  env_modtypes : module_type_body MPmap.t;
-  env_alias : module_path MPmap.t }
+  env_modtypes : module_type_body MPmap.t}
 
 type stratification = {
   env_universes : universes;
@@ -25,11 +24,10 @@ type env = {
 
 let empty_env = {
   env_globals =
-  { env_constants = Cmap.empty;
-    env_inductives = KNmap.empty;
+  { env_constants = Cmap_env.empty;
+    env_inductives = Mindmap_env.empty;
     env_modules = MPmap.empty;
-    env_modtypes = MPmap.empty;
-    env_alias = MPmap.empty };
+    env_modtypes = MPmap.empty};
   env_named_context = [];
   env_rel_context = [];
   env_stratification =
@@ -108,11 +106,11 @@ let add_constraints c env =
 (* Global constants *)
 
 let lookup_constant kn env =
-  Cmap.find kn env.env_globals.env_constants
+  Cmap_env.find kn env.env_globals.env_constants
 
 let add_constant kn cs env =
   let new_constants =
-    Cmap.add kn cs env.env_globals.env_constants in
+    Cmap_env.add kn cs env.env_globals.env_constants in
   let new_globals =
     { env.env_globals with
 	env_constants = new_constants } in
@@ -145,26 +143,15 @@ let evaluable_constant cst env =
 
 (* Mutual Inductives *)
 let lookup_mind kn env =
-  KNmap.find kn env.env_globals.env_inductives
-
-let rec scrape_mind env kn =
-  match (lookup_mind kn env).mind_equiv with
-    | None -> kn
-    | Some kn' -> scrape_mind env kn'
+  Mindmap_env.find kn env.env_globals.env_inductives
 
 let add_mind kn mib env =
-  let new_inds = KNmap.add kn mib env.env_globals.env_inductives in
+  let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in
   let new_globals =
     { env.env_globals with
 	env_inductives = new_inds } in
   { env with env_globals = new_globals }
 
-let rec mind_equiv env (kn1,i1) (kn2,i2) =
-  let rec equiv kn1 kn2 =
-    kn1 = kn2 ||
-    scrape_mind env kn1 = scrape_mind env kn2 in
-  i1 = i2 && equiv kn1 kn2
-
 
 (* Modules *)
 
@@ -182,19 +169,6 @@ let shallow_add_module mp mb env =
 	env_modules = new_mods } in
   { env with env_globals = new_globals }
 
-let register_alias mp1 mp2 env =
-  let new_alias =  MPmap.add mp1 mp2 env.env_globals.env_alias in
-  let new_globals =
-    { env.env_globals with
-	env_alias = new_alias } in
-    { env with env_globals = new_globals }
-
-let rec scrape_alias mp env =
-  try
-    let mp1 = MPmap.find mp env.env_globals.env_alias in
-      scrape_alias mp1 env
-  with
-      Not_found -> mp
 
 let lookup_module mp env =
   MPmap.find mp env.env_globals.env_modules
diff --git a/checker/environ.mli b/checker/environ.mli
index 1541bf0d8..776698ed8 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -4,12 +4,10 @@ open Term
 (* Environments *)
 
 type globals = {
-  env_constants : Declarations.constant_body Cmap.t;
-  env_inductives : Declarations.mutual_inductive_body KNmap.t;
+  env_constants : Declarations.constant_body Cmap_env.t;
+  env_inductives : Declarations.mutual_inductive_body Mindmap_env.t;
   env_modules : Declarations.module_body MPmap.t;
-  env_modtypes : Declarations.module_type_body MPmap.t;
-  env_alias : module_path MPmap.t;
-}
+  env_modtypes : Declarations.module_type_body MPmap.t}
 type stratification = {
   env_universes : Univ.universes;
   env_engagement : Declarations.engagement option;
@@ -61,17 +59,14 @@ val evaluable_constant : constant -> env -> bool
 (* Inductives *)
 val lookup_mind :
   mutual_inductive -> env -> Declarations.mutual_inductive_body
-val scrape_mind : env -> mutual_inductive -> mutual_inductive
+
 val add_mind :
   mutual_inductive -> Declarations.mutual_inductive_body -> env -> env
-val mind_equiv : env -> inductive -> inductive -> bool
 
 (* Modules *)
 val add_modtype :
   module_path -> Declarations.module_type_body -> env -> env
 val shallow_add_module :
   module_path -> Declarations.module_body -> env -> env
-val register_alias : module_path -> module_path -> env -> env
-val scrape_alias : module_path -> env -> module_path
 val lookup_module : module_path -> env -> Declarations.module_body
 val lookup_modtype : module_path -> env -> Declarations.module_type_body
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 3d4f6be79..e0aa9e7c3 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -22,13 +22,11 @@ open Environ
 let rec debug_string_of_mp = function
   | MPfile sl -> string_of_dirpath sl
   | MPbound uid -> "bound("^string_of_mbid uid^")"
-  | MPself uid -> "self("^string_of_msid uid^")"
   | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l
 
 let rec string_of_mp = function
   | MPfile sl -> string_of_dirpath sl
   | MPbound uid -> string_of_mbid uid
-  | MPself uid -> string_of_msid uid
   | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l
 
 let string_of_mp mp =
@@ -515,7 +513,7 @@ let check_positivity env_ar params nrecp inds =
 (************************************************************************)
 
 let check_inductive env kn mib =
-  Flags.if_verbose msgnl (str "  checking ind: " ++ prkn kn);
+  Flags.if_verbose msgnl (str "  checking ind: " ++ pr_mind kn);
   (* check mind_constraints: should be consistent with env *)
   let env = add_constraints mib.mind_constraints env in
   (* check mind_record : TODO ? check #constructor = 1 ? *)
@@ -540,8 +538,6 @@ let check_inductive env kn mib =
   (* check mind_nparams_rec: positivity condition *)
   check_positivity env_ar params mib.mind_nparams_rec mib.mind_packets;
   (* check mind_equiv... *)
-  if mib.mind_equiv <> None then
-    msg_warning (str"TODO: mind_equiv not checked");
   (* Now we can add the inductive *)
   add_mind kn mib env
 
diff --git a/checker/inductive.ml b/checker/inductive.ml
index e08efbe5b..19c7a6cfe 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -351,7 +351,7 @@ let type_case_branches env (ind,largs) (p,pj) c =
 let check_case_info env indsp ci =
   let (mib,mip) = lookup_mind_specif env indsp in
   if
-    not (mind_equiv env indsp ci.ci_ind) or
+    not (eq_ind indsp ci.ci_ind) or
     (mib.mind_nparams <> ci.ci_npar) or
     (mip.mind_consnrealdecls <> ci.ci_cstr_nargs)
   then raise (TypeError(env,WrongCaseInfo(indsp,ci)))
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 99babe632..e95109fc5 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -65,10 +65,6 @@ 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 check_alias (s1:substitution) s2 =
-  if s1 <> s2 then failwith "Incorrect alias"
-
 let check_definition_sub env cb1 cb2 =
   let check_type env t1 t2 =
 
@@ -135,31 +131,31 @@ let lookup_modtype mp env =
   with Not_found ->
     failwith ("Unknown module type: "^string_of_mp mp)
 
-
-let rec check_with env mtb with_decl =
+let rec check_with env mtb with_decl mp=
   match with_decl with
     | With_definition_body _ ->
-	check_with_aux_def env mtb with_decl;
-	empty_subst
+	check_with_aux_def env mtb with_decl mp;
+	mtb
     | With_module_body _ ->
-	check_with_aux_mod env mtb with_decl
+	check_with_aux_mod env mtb with_decl mp;
+	mtb
 
-and check_with_aux_def env mtb with_decl =
-  let msid,sig_b = match (eval_struct env mtb) with
-    | SEBstruct(msid,sig_b) ->
-	msid,sig_b
+and check_with_aux_def env mtb with_decl mp =
+  let sig_b = match mtb with
+    | SEBstruct(sig_b) ->
+	sig_b
     | _ -> error_signature_expected mtb
   in
   let id,idl = match with_decl with
-    | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_,_) ->
+    | With_definition_body (id::idl,_) | With_module_body (id::idl,_) ->
                                            id,idl
-    | With_definition_body ([],_) | With_module_body ([],_,_,_) -> assert false
+    | With_definition_body ([],_) | With_module_body ([],_) -> assert false
   in
   let l = label_of_id id in
     try
       let rev_before,spec,after = list_split_assoc l [] sig_b in
       let before = List.rev rev_before in
-      let env' = Modops.add_signature (MPself msid) before env in
+      let env' = Modops.add_signature mp before empty_delta_resolver env in
 	match with_decl with
           | With_definition_body ([],_) -> assert false
 	  | With_definition_body ([id],c) ->
@@ -179,9 +175,9 @@ and check_with_aux_def env mtb with_decl =
 			let new_with_decl = match with_decl with
 			    With_definition_body (_,c) ->
                               With_definition_body (idl,c)
-			  | With_module_body (_,c,t,cst) ->
-                              With_module_body (idl,c,t,cst) in
-			  check_with_aux_def env' (type_of_mb env old) new_with_decl
+			  | With_module_body (_,c) ->
+                              With_module_body (idl,c) in
+			  check_with_aux_def env' old.mod_type new_with_decl (MPdot(mp,l))
                     | Some msb ->
 			error_a_generative_module_expected l
 		end
@@ -190,46 +186,35 @@ and check_with_aux_def env mtb with_decl =
 	Not_found -> error_no_such_label l
       | Reduction.NotConvertible -> error_with_incorrect l
 
-and check_with_aux_mod env mtb with_decl =
-  let initmsid,msid,sig_b =
-    match eval_struct env mtb with
-    | SEBstruct(msid,sig_b) ->
-        let msid'=(refresh_msid msid) in
-	msid,msid',(subst_signature_msid msid (MPself(msid')) sig_b)
+and check_with_aux_mod env mtb with_decl mp =
+  let sig_b =
+    match mtb with
+    | SEBstruct(sig_b) ->
+	sig_b
     | _ -> error_signature_expected mtb in
   let id,idl = match with_decl with
-    | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_,_) ->
+    | With_definition_body (id::idl,_) | With_module_body (id::idl,_) ->
         id,idl
-    | With_definition_body ([],_) | With_module_body ([],_,_,_) -> assert false
+    | With_definition_body ([],_) | With_module_body ([],_) -> assert false
   in
   let l = label_of_id id in
     try
       let rev_before,spec,after = list_split_assoc l [] sig_b in
       let before = List.rev rev_before in
       let rec mp_rec = function
-	| [] -> MPself initmsid
+	| [] -> mp
 	| i::r -> MPdot(mp_rec r,label_of_id i)
       in
-      let env' = Modops.add_signature (MPself msid) before env in
+      let env' = Modops.add_signature mp before empty_delta_resolver env in
 	match with_decl with
-          | With_module_body ([],_,_,_) -> assert false
-	  | With_module_body ([id], mp,_,_) ->
-	      let old,alias = match spec with
-		  SFBmodule msb -> Some msb,None
-		| SFBalias (mp',_,_) -> None,Some mp'
+          | With_module_body ([],_) -> assert false
+	  | With_module_body ([id], mp1) ->
+	      let _ = match spec with
+		  SFBmodule msb -> msb
 		| _ -> error_not_a_module l
 	      in
-	      let mtb' = lookup_modtype mp env' in
-	      let _ =
-		match old,alias with
-		    Some msb,None -> ()
-		  | None,Some mp' ->
-		      check_modpath_equiv env' mp mp'
-		  | _,_ ->
-		      anomaly "Mod_typing:no implementation and no alias"
-	      in
-		join (map_mp (mp_rec [id]) mp) mtb'.typ_alias
-        | With_module_body (_::_,mp,_,_) ->
+	      let _ = (lookup_module mp1 env) in ()
+        | With_module_body (_::_,mp) ->
 	    let old = match spec with
 		SFBmodule msb -> msb
 	      | _ -> error_not_a_module l
@@ -240,12 +225,10 @@ and check_with_aux_mod env mtb with_decl =
                       let new_with_decl = match with_decl with
 			  With_definition_body (_,c) ->
 			    With_definition_body (idl,c)
-			| With_module_body (_,c,t,cst) ->
-                            With_module_body (idl,c,t,cst) in
-		      let sub =
-			check_with_aux_mod env'
-			  (type_of_mb env old) new_with_decl in
-		      join (map_mp (mp_rec idl) mp) sub
+			| With_module_body (_,c) ->
+                            With_module_body (idl,c) in
+		 	check_with_aux_mod env'
+			  old.mod_type new_with_decl (MPdot(mp,l))
                   | Some msb ->
                       error_a_generative_module_expected l
               end
@@ -255,110 +238,105 @@ and check_with_aux_mod env mtb with_decl =
       | Reduction.NotConvertible -> error_with_incorrect l
 
 and check_module_type env mty =
-  if mty.typ_strength <> None then
-    failwith "strengthening of module types not supported";
-  let sub = check_modexpr env mty.typ_expr in
-  check_alias mty.typ_alias sub
-
-and check_module env mb =
-  let sub =
-    match mb.mod_expr, mb.mod_type with
-      | None, None ->
-	  anomaly "Mod_typing.translate_module: empty type and expr in module entry"
-      | None, Some mtb -> check_modexpr env mtb
-
-      | Some mexpr, _ ->
-	  let sub1 = check_modexpr env mexpr in
-	  (match mb.mod_type with
-	    | None ->  sub1
-	    | Some mte ->
-		let sub2 = check_modexpr env mte in
-                check_subtypes env
-		  {typ_expr = mexpr;
-		   typ_strength = None;
-		   typ_alias = sub1;}
-		  {typ_expr = mte;
-		   typ_strength = None;
-		   typ_alias = sub2;};
-		sub2) in
-  check_alias mb.mod_alias sub
-
-and check_structure_field (s,env) mp lab = function
+  let _ = check_modtype env mty.typ_expr mty.typ_mp in ()
+
+							 
+and check_module env mp mb =
+  match mb.mod_expr, mb.mod_type with
+    | None,mtb -> 
+	let _ = check_modtype env mtb mb.mod_mp in ()
+    | Some mexpr, _ ->
+	let sign = check_modexpr env mexpr mb.mod_mp in
+	let _ = check_modtype env mb.mod_type mb.mod_mp in
+          check_subtypes env 
+	    {typ_mp=mp;
+	     typ_expr=sign;
+	     typ_expr_alg=None;
+	     typ_constraints=Univ.Constraint.empty;
+	     typ_delta = empty_delta_resolver;}
+	    {typ_mp=mp;
+	     typ_expr=mb.mod_type;
+	     typ_expr_alg=None;
+	     typ_constraints=Univ.Constraint.empty;
+	     typ_delta = empty_delta_resolver;};
+	  
+and check_structure_field env mp lab = function
   | SFBconst cb ->
       let c = make_con mp empty_dirpath lab in
-      (s,check_constant_declaration env c cb)
+	check_constant_declaration env c cb
   | SFBmind mib ->
-      let kn = make_kn mp empty_dirpath lab in
-      (s,Indtypes.check_inductive env kn mib)
+      let kn = make_mind mp empty_dirpath lab in
+	Indtypes.check_inductive env kn mib
   | SFBmodule msb ->
-      check_module env msb;
-      let mp1 = MPdot(mp,lab) in
-      let is_fun, sub = Modops.update_subst env msb mp1 in
-      ((if is_fun then s else join s sub),
-       Modops.add_module (MPdot(mp,lab)) msb env)
-  | SFBalias(mp2,_,cst) ->
-      (* cf Safe_typing.add_alias *)
-      (try
-        let mp' = MPdot(mp,lab) in
-        let mp2' = scrape_alias mp2 env in
-        let _,sub = Modops.update_subst env (lookup_module mp2' env) mp2' in
-        let sub = update_subst sub (map_mp mp' mp2') in
-        let sub = join_alias sub (map_mp mp' mp2') in
-        let sub = add_mp mp' mp2' sub in
-        (join s sub, register_alias mp' mp2 env)
-      with Not_found -> failwith "unkown aliased module")
+      let _= check_module env (MPdot(mp,lab)) msb in
+	Modops.add_module msb env
   | SFBmodtype mty ->
-      let kn = MPdot(mp, lab) in
       check_module_type env mty;
-      (join s mty.typ_alias, add_modtype kn mty env)
-
-and check_modexpr env mse = match mse with
+      add_modtype (MPdot(mp,lab)) mty env
+	
+and check_modexpr env mse mp_mse = match mse with
+  | SEBident mp ->
+      let mb = lookup_module mp env in
+      	(subst_and_strengthen mb mp_mse env).mod_type
+  | SEBfunctor (arg_id, mtb, body) ->
+      check_module_type env mtb ;
+      let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in
+      let sign = check_modexpr env' body mp_mse in
+	SEBfunctor (arg_id, mtb, sign)
+  | SEBapply (f,m,cst) ->
+      let sign = check_modexpr env f mp_mse in
+      let farg_id, farg_b, fbody_b = destr_functor env sign in
+      let mp =
+	try (path_of_mexpr m)
+	with Not_path -> error_application_to_not_path m
+	  (* place for nondep_supertype *) in
+      let mtb = module_type_of_module env (Some mp) (lookup_module mp env) in
+	check_subtypes env mtb farg_b;
+	(subst_struct_expr (map_mbid farg_id mp) fbody_b)
+  | SEBwith(mte, with_decl) ->
+      let sign = check_modexpr env mte mp_mse in
+      let sign = check_with env sign with_decl mp_mse in 
+	sign
+  | SEBstruct(msb) ->
+      let _ = List.fold_left (fun env (lab,mb) ->
+		   check_structure_field env mp_mse lab mb) env msb in
+	SEBstruct(msb)
+	
+and check_modtype env mse mp_mse= match mse with
   | SEBident mp ->
-      let mp = scrape_alias mp env in
       let mtb = lookup_modtype mp env in
-      mtb.typ_alias
+	mtb.typ_expr
   | SEBfunctor (arg_id, mtb, body) ->
       check_module_type env mtb;
-      let env' = add_module (MPbound arg_id) (module_body_of_type mtb) env in
-      let sub = check_modexpr env' body in
-      sub
+      let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in
+      let body = check_modtype env' body mp_mse in
+	SEBfunctor(arg_id,mtb,body)
   | SEBapply (f,m,cst) ->
-      let sub1 = check_modexpr env f in
-      let f'= eval_struct env f in
-      let farg_id, farg_b, fbody_b = destr_functor env f' in
+      let sign = check_modtype env f mp_mse in
+      let farg_id, farg_b, fbody_b = destr_functor env sign in
       let mp =
-	try scrape_alias (path_of_mexpr m) env
+	try (path_of_mexpr m)
 	with Not_path -> error_application_to_not_path m
-	      (* place for nondep_supertype *) in
-      let mtb = lookup_modtype mp env in
-      check_subtypes env mtb farg_b;
-      let sub2 = match eval_struct env m with
-	| SEBstruct (msid,sign) ->
-	    join_alias
-	      (subst_key (map_msid msid mp) mtb.typ_alias)
-	      (map_msid msid mp)
-	| _ -> mtb.typ_alias in
-      let sub3 = join_alias sub1 (map_mbid farg_id mp) in
-      let sub4 = update_subst sub2 sub3 in
-      join sub3 sub4
+	  (* place for nondep_supertype *) in
+      let mtb = module_type_of_module env (Some mp) (lookup_module mp env) in
+	check_subtypes env mtb farg_b;
+	subst_struct_expr (map_mbid farg_id mp) fbody_b
   | SEBwith(mte, with_decl) ->
-	let sub1 = check_modexpr env mte in
-	let sub2 = check_with env mte with_decl in
-	join sub1 sub2
-  | SEBstruct(msid,msb) ->
-      let mp = MPself msid in
-      let (sub,_) =
-        List.fold_left (fun env (lab,mb) ->
-          check_structure_field env mp lab mb) (empty_subst,env) msb in
-      sub
-
+      let sign = check_modtype env mte mp_mse in
+      let sign = check_with env sign with_decl mp_mse in
+	sign
+  | SEBstruct(msb) ->
+      let _ = List.fold_left (fun env (lab,mb) ->
+		   check_structure_field env mp_mse lab mb) env msb in
+      SEBstruct(msb)
+	
 (*
-let rec add_struct_expr_constraints env = function
+  let rec add_struct_expr_constraints env = function
   | SEBident _ -> env
-
+  
   | SEBfunctor (_,mtb,meb) ->
-      add_struct_expr_constraints
-	(add_modtype_constraints env mtb) meb
+  add_struct_expr_constraints
+  (add_modtype_constraints env mtb) meb
 
   | SEBstruct (_,structure_body) ->
       List.fold_left
diff --git a/checker/modops.ml b/checker/modops.ml
index a986e1898..3d07135d1 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -32,11 +32,10 @@ let error_not_match l _ =
 
 let error_no_such_label l = error ("No such label "^string_of_label l)
 
-let error_no_such_label_sub l l1 l2 =
-  let l1 = string_of_msid l1 in
-  let l2 = string_of_msid l2 in
-  error (l1^" is not a subtype of "^l2^".\nThe field "^
-         string_of_label l^" is missing (or invisible) in "^l1^".")
+let error_no_such_label_sub l l1 =
+  let l1 = string_of_mp l1 in
+  error ("The field "^
+         string_of_label l^" is missing in "^l1^".")
 
 let error_not_a_module_loc loc s =
   user_err_loc (loc,"",str ("\""^string_of_label s^"\" is not a module"))
@@ -56,38 +55,6 @@ let error_signature_expected mtb =
 
 let error_application_to_not_path _ = error "Application to not path"
 
-
-let module_body_of_type mtb =
-  { mod_type = Some mtb.typ_expr;
-    mod_expr = None;
-    mod_constraints = Constraint.empty;
-    mod_alias = mtb.typ_alias;
-    mod_retroknowledge = []}
-
-let module_type_of_module mp mb =
-  {typ_expr =
-      (match mb.mod_type with
-	| Some expr -> expr
-	| None -> (match mb.mod_expr with
-		     | Some expr -> expr
-		     | None ->
-			 anomaly "Modops: empty expr and type"));
-   typ_alias = mb.mod_alias;
-   typ_strength = mp
-  }
-
-
-
-let rec list_split_assoc k rev_before = function
-  | [] -> raise Not_found
-  | (k',b)::after when k=k' -> rev_before,b,after
-  | h::tail -> list_split_assoc k (h::rev_before) tail
-
-let path_of_seb = function
-  | SEBident mp -> mp
-  | _ -> anomaly "Modops: evaluation failed."
-
-
 let destr_functor env mtb =
   match mtb with
   | SEBfunctor (arg_id,arg_t,body_t) ->
@@ -95,254 +62,157 @@ let destr_functor env mtb =
   | _ -> error_not_a_functor mtb
 
 
-let rec check_modpath_equiv env mp1 mp2 =
-  if mp1=mp2 then () else
-  let mp1 = scrape_alias mp1 env in
-  let mp2 = scrape_alias mp2 env in
-    if mp1=mp2 then ()
-    else
-      error_not_equal mp1 mp2
-
-
-
-let strengthen_const env mp l cb =
-  match cb.const_opaque, cb.const_body with
-  | false, Some _ -> cb
-  | true, Some _
-  | _, None ->
-      let const = Const (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
-	}
-
-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)}
-
+let is_functor = function
+ | SEBfunctor (arg_id,arg_t,body_t) -> true
+ | _ -> false
 
-let rec eval_struct env = function
-  | SEBident mp ->
-      begin
-        let mp = scrape_alias mp env in
-	let mtb =lookup_modtype mp env in
-	match mtb.typ_expr,mtb.typ_strength with
-	    mtb,None -> eval_struct env mtb
-	  | mtb,Some mp -> strengthen_mtb env mp (eval_struct env mtb)
-      end
-  | SEBapply (seb1,seb2,_) ->
-      let svb1 = eval_struct env seb1 in
-      let farg_id, farg_b, fbody_b = destr_functor env svb1 in
-      let mp = path_of_seb seb2 in
-      let mp = scrape_alias mp env in
-      let sub_alias = (lookup_modtype mp env).typ_alias in
-      let sub_alias = match eval_struct env (SEBident mp) with
-	  | SEBstruct (msid,sign) -> subst_key (map_msid msid mp) sub_alias
-	  | _ -> sub_alias in
-      let sub_alias = update_subst_alias sub_alias
-	(map_mbid farg_id mp) in
-	eval_struct env (subst_struct_expr
-			   (join sub_alias (map_mbid farg_id mp)) fbody_b)
-  | SEBwith (mtb,(With_definition_body _ as wdb)) ->
-      merge_with env mtb wdb empty_subst
-  | SEBwith (mtb, (With_module_body (_,mp,_,_) as wdb)) ->
-      let alias_in_mp =
-	(lookup_modtype mp env).typ_alias in
-	merge_with env mtb wdb alias_in_mp
-(*  | SEBfunctor(mbid,mtb,body) ->
-      let env = add_module (MPbound mbid) (module_body_of_type mtb) env in
-	SEBfunctor(mbid,mtb,eval_struct env body) *)
-  | mtb -> mtb
-
-and type_of_mb env mb =
-  match mb.mod_type,mb.mod_expr with
-      None,Some b -> eval_struct env b
-    | Some t, _ -> eval_struct env t
-    | _,_ -> anomaly
-	"Modops:  empty type and empty expr"
+let module_body_of_type mp mtb = 
+  { mod_mp = mp;
+    mod_type = mtb.typ_expr;
+    mod_type_alg = mtb.typ_expr_alg;
+    mod_expr = None;
+    mod_constraints = mtb.typ_constraints;
+    mod_delta = mtb.typ_delta;
+    mod_retroknowledge = []}
 
-and merge_with env mtb with_decl alias=
-  let msid,sig_b = match (eval_struct env mtb) with
-    | SEBstruct(msid,sig_b) -> msid,sig_b
-    | _ -> 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
-  in
-  let l = label_of_id id in
-    try
-      let rev_before,spec,after = list_split_assoc l [] sig_b in
-      let before = List.rev rev_before in
-      let rec mp_rec = function
-	| [] -> MPself msid
-	| i::r -> MPdot(mp_rec r,label_of_id i)
-      in
-      let new_spec,subst = match with_decl with
-        | With_definition_body ([],_)
-        | With_module_body ([],_,_,_) -> assert false
-	| With_definition_body ([id],c) ->
-	    SFBconst c,None
-	| With_module_body ([id], mp,typ_opt,cst) ->
-	    let mp' = scrape_alias mp env in
-	      SFBalias (mp,typ_opt,Some cst),
-	    Some(join (map_mp (mp_rec [id]) mp') alias)
-	| With_definition_body (_::_,_)
-        | With_module_body (_::_,_,_,_) ->
-	    let old = match spec with
-		SFBmodule msb -> msb
-	      | _ -> error_not_a_module 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,t,cst) ->
-		    With_module_body (idl,mp,t,cst),
-		      Some(map_mp (mp_rec idc) mp)
-	    in
-	    let subst = Option.fold_right join subst1 alias in
-            let modtype =
-              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 = subst;
-		mod_retroknowledge = old.mod_retroknowledge}
-	    in
-	      (SFBmodule msb),Some subst
-      in
-	SEBstruct(msid,  before@(l,new_spec)::
-		    (Option.fold_right subst_structure subst after))
-    with
-	Not_found -> error_no_such_label l
+let check_modpath_equiv env mp1 mp2 = 
+  if mp1=mp2 then () else
+ (*   let mb1=lookup_module  mp1 env in
+    let mb2=lookup_module mp2 env in
+      if (delta_of_mp mb1.mod_delta mp1)=(delta_of_mp mb2.mod_delta mp2)
+      then ()
+      else*) error_not_equal mp1 mp2
 
-and add_signature mp sign env =
+let rec add_signature mp sign resolver env = 
   let add_one env (l,elem) =
     let kn = make_kn mp empty_dirpath l in
-    let con = make_con mp empty_dirpath l in
+    let con = constant_of_kn kn in
+    let mind = mind_of_kn kn in
       match elem with
-	| SFBconst cb -> Environ.add_constant con cb env
-	| SFBmind mib -> Environ.add_mind kn mib env
-	| SFBmodule mb ->
-	    add_module (MPdot (mp,l)) mb env
+	| SFBconst cb -> 
+	   (* let con =  constant_of_delta resolver con in*)
+	      Environ.add_constant con cb env
+	| SFBmind mib -> 
+	   (* let mind =  mind_of_delta resolver mind in*)
+	    Environ.add_mind mind mib env
+	| SFBmodule mb -> add_module mb env
 	      (* adds components as well *)
-	| SFBalias (mp1,_,cst) ->
-	    Environ.register_alias (MPdot(mp,l)) mp1 env
-	| SFBmodtype mtb -> Environ.add_modtype (MPdot(mp,l))
-	    mtb env
+	| SFBmodtype mtb -> Environ.add_modtype mtb.typ_mp mtb env
   in
     List.fold_left add_one env sign
 
-and add_module mp mb env =
+and add_module mb env = 
+  let mp = mb.mod_mp in
   let env = Environ.shallow_add_module mp mb env in
-  let env =
-    Environ.add_modtype mp (module_type_of_module (Some mp) mb) env
-  in
-  let mod_typ = type_of_mb env mb in
-    match mod_typ with
-      | SEBstruct (msid,sign) ->
-	  add_signature mp (subst_signature_msid msid mp sign) env
+    match mb.mod_type with
+      | SEBstruct (sign) -> 
+	    add_signature mp sign mb.mod_delta env
       | SEBfunctor _ -> env
       | _ -> anomaly "Modops:the evaluation of the structure failed "
 
 
-
-and  constants_of_specification env mp sign =
- let aux (env,res) (l,elem) =
-  match elem with
-   | SFBconst cb -> env,((make_con mp empty_dirpath l),cb)::res
-   | SFBmind _ -> env,res
-   | SFBmodule mb ->
-       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) ->
-       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
-   | SFBmodtype mtb ->
-       (* module type dans un module type.
-	  Il faut au moins mettre mtb dans l'environnement (avec le bon
-	  kn pour pouvoir continuer aller deplier les modules utilisant ce
-	  mtb
-	  ex:
-	  Module Type T1.
-	  Module Type T2.
-	     ....
-    	    End T2.
-	  .....
-            Declare Module M : T2.
-         End T2
-	  si on ne rajoute pas T2 dans l'environement de typage
-	  on va exploser au moment du Declare Module
-       *)
-       let new_env = Environ.add_modtype (MPdot(mp,l)) mtb env in
-       new_env, (constants_of_modtype env (MPdot(mp,l)) mtb.typ_expr) @ res
- in
- snd (List.fold_left aux (env,[]) sign)
-
-and constants_of_modtype env mp modtype =
-  match (eval_struct env modtype) with
-      SEBstruct (msid,sign) ->
-	constants_of_specification env mp
-	  (subst_signature_msid msid mp sign)
-    | SEBfunctor _ -> []
-    | _ -> anomaly "Modops:the evaluation of the structure failed "
-
-and strengthen_mtb env mp mtb =
-  let mtb1 = eval_struct env mtb in
-  match  mtb1 with
-  | SEBfunctor _ -> mtb1
-  | SEBstruct (msid,sign) ->
-      SEBstruct (msid,strengthen_sig env msid sign mp)
-  | _ -> anomaly "Modops:the evaluation of the structure failed "
-
-and strengthen_mod env mp mb =
-  let mod_typ = type_of_mb env mb in
-    { mod_expr = mb.mod_expr;
-      mod_type = Some (strengthen_mtb env mp mod_typ);
-      mod_constraints = mb.mod_constraints;
-      mod_alias = mb.mod_alias;
-      mod_retroknowledge = mb.mod_retroknowledge}
-
-and strengthen_sig env msid sign mp = match sign with
-  | [] -> []
-  | (l,SFBconst cb) :: rest ->
-      let item' = l,SFBconst (strengthen_const env mp l cb) in
-      let rest' = strengthen_sig env msid rest mp in
-	item'::rest'
-  | (l,SFBmind mib) :: rest ->
-      let item' = l,SFBmind (strengthen_mind env mp l mib) in
-      let rest' = strengthen_sig env msid rest mp in
-	item'::rest'
-  | (l,SFBmodule mb) :: rest ->
-      let mp' = MPdot (mp,l) in
-	let item' = l,SFBmodule (strengthen_mod env mp' mb) in
-	let env' = add_module
-	  (MPdot (MPself msid,l)) mb env in
-        let rest' = strengthen_sig env' msid rest mp in
+let strengthen_const env mp_from l cb resolver = 
+  match cb.const_opaque, cb.const_body with
+  | false, Some _ -> cb
+  | true, Some _ 
+  | _, None ->
+      let con = make_con mp_from empty_dirpath l in
+     (* let con =  constant_of_delta resolver con in*)
+      let const = Const con in 
+      let const_subs = Some (Declarations.from_val const) in
+	{cb with 
+	   const_body = const_subs;
+	   const_opaque = false;
+	}
+	  
+
+let rec strengthen_mod env mp_from mp_to mb = 
+  assert(mp_from = mb.mod_mp);
+(*  if mp_in_delta mb.mod_mp mb.mod_delta then
+    mb 
+  else*)
+    match mb.mod_type with
+     | SEBstruct (sign) -> 
+	 let resolve_out,sign_out = 
+	   strengthen_sig env mp_from sign mp_to mb.mod_delta in
+	   { mb with
+	       mod_expr = Some (SEBident mp_to);
+	       mod_type = SEBstruct(sign_out);
+	       mod_type_alg = mb.mod_type_alg;
+	       mod_constraints = mb.mod_constraints;
+	       mod_delta = resolve_out(*add_mp_delta_resolver mp_from mp_to 
+	       (add_delta_resolver mb.mod_delta resolve_out)*);
+	       mod_retroknowledge = mb.mod_retroknowledge}
+     | SEBfunctor _ -> mb
+     | _ -> anomaly "Modops:the evaluation of the structure failed "
+	 
+and strengthen_sig env mp_from sign mp_to resolver =
+  match sign with
+    | [] -> empty_delta_resolver,[]
+    | (l,SFBconst cb) :: rest ->
+	let item' = 
+	  l,SFBconst (strengthen_const env mp_from l cb resolver) in
+	let resolve_out,rest' =
+	  strengthen_sig env mp_from rest mp_to resolver in
+	  resolve_out,item'::rest'
+    | (_,SFBmind _ as item):: rest ->
+	let resolve_out,rest' = 
+	  strengthen_sig env mp_from rest mp_to resolver in
+	  resolve_out,item::rest'
+    | (l,SFBmodule mb) :: rest ->
+	let mp_from' = MPdot (mp_from,l) in
+	let mp_to' = MPdot(mp_to,l) in 
+	let mb_out = 
+	  strengthen_mod env mp_from' mp_to' mb in
+	let item' = l,SFBmodule (mb_out) in
+	let env' = add_module mb_out env in
+	let resolve_out,rest' = 
+	  strengthen_sig env' mp_from rest mp_to resolver in
+	  resolve_out
+	  (*add_delta_resolver resolve_out mb.mod_delta*),
 	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'
-  | (l,SFBmodtype mty as item) :: rest ->
-      let env' = add_modtype
-		   (MPdot((MPself msid),l))
-		   mty
-		   env
-      in
-      let rest' = strengthen_sig env' msid rest mp in
-	item::rest'
-
-
-let strengthen env mtb mp = strengthen_mtb env mp mtb
+    | (l,SFBmodtype mty as item) :: rest -> 
+	let env' = add_modtype 
+	  (MPdot(mp_from,l)) mty env
+	in
+	let resolve_out,rest' = 
+	  strengthen_sig env' mp_from rest mp_to resolver in
+	  resolve_out,item::rest'
+    
+let strengthen env mtb mp = 
+(*  if mp_in_delta mtb.typ_mp mtb.typ_delta then
+    (* in this case mtb has already been strengthened*)
+    mtb 
+  else*)
+    match mtb.typ_expr with
+      | SEBstruct (sign) -> 
+	  let resolve_out,sign_out =
+	    strengthen_sig env mtb.typ_mp sign mp mtb.typ_delta in
+	    {mtb with
+	       typ_expr = SEBstruct(sign_out);
+	       typ_delta = resolve_out(*add_delta_resolver mtb.typ_delta
+		(add_mp_delta_resolver mtb.typ_mp mp resolve_out)*)}
+      | SEBfunctor _ -> mtb
+      | _ -> anomaly "Modops:the evaluation of the structure failed "
 
-let update_subst env mb mp =
-  match type_of_mb env mb with
-    | SEBstruct(msid,str) -> false, join_alias
-	(subst_key (map_msid msid mp) mb.mod_alias)
-	(map_msid msid mp)
-    | _ -> true, mb.mod_alias
+let subst_and_strengthen mb mp env =
+  strengthen_mod env mb.mod_mp mp 
+    (subst_module (map_mp mb.mod_mp mp) mb)
+
+
+let module_type_of_module env mp mb =
+  match mp with
+      Some mp ->
+	strengthen env {
+	  typ_mp = mp;
+	  typ_expr = mb.mod_type;
+	  typ_expr_alg = None;
+	  typ_constraints = mb.mod_constraints;
+	  typ_delta = mb.mod_delta} mp
+	  
+    | None ->
+	{typ_mp = mb.mod_mp;
+	 typ_expr = mb.mod_type;
+	 typ_expr_alg = None;
+	 typ_constraints = mb.mod_constraints;
+	 typ_delta = mb.mod_delta}
diff --git a/checker/modops.mli b/checker/modops.mli
index d5c9f4de6..4476013c6 100644
--- a/checker/modops.mli
+++ b/checker/modops.mli
@@ -19,33 +19,25 @@ open Environ
 
 (* Various operations on modules and module types *)
 
-(* make the environment entry out of type *)
-val module_body_of_type : module_type_body -> module_body
+(* make the envirconment entry out of type *)
+val module_body_of_type : module_path -> module_type_body -> module_body
 
-val module_type_of_module : module_path option -> module_body ->
+val module_type_of_module : env -> module_path option -> module_body ->
   module_type_body
 
 val destr_functor :
   env -> struct_expr_body -> mod_bound_id * module_type_body * struct_expr_body
 
-(* Evaluation functions *)
-val eval_struct : env -> struct_expr_body -> struct_expr_body
-
-val type_of_mb : env -> module_body -> struct_expr_body
-
-(* [add_signature mp sign env] assumes that the substitution [msid]
-   $\mapsto$ [mp] has already been performed (or is not necessary, like
-   when [mp = MPself msid]) *)
-val add_signature : module_path -> structure_body -> env -> env
+val add_signature : module_path -> structure_body -> delta_resolver -> env -> env
 
 (* adds a module and its components, but not the constraints *)
-val add_module : module_path -> module_body ->  env -> env
+val add_module : module_body ->  env -> env
 
 val check_modpath_equiv : env -> module_path -> module_path -> unit
 
-val strengthen : env -> struct_expr_body -> module_path -> struct_expr_body
+val strengthen : env -> module_type_body -> module_path -> module_type_body
 
-val update_subst : env -> module_body -> module_path -> bool * substitution
+val subst_and_strengthen : module_body -> module_path -> env -> module_body 
 
 val error_incompatible_modtypes :
   module_type_body -> module_type_body -> 'a
@@ -57,7 +49,7 @@ val error_with_incorrect : label -> 'a
 val error_no_such_label : label -> 'a
 
 val error_no_such_label_sub :
-  label -> mod_self_id -> mod_self_id -> 'a
+  label -> module_path -> 'a
 
 val error_signature_expected : struct_expr_body -> 'a
 
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index b0d683ff3..da0e63c23 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -30,9 +30,8 @@ let set_engagement c =
 (* full_add_module adds module with universes and constraints *)
 let full_add_module dp mb digest =
   let env = !genv in
-  let mp = MPfile dp in
   let env = add_constraints mb.mod_constraints env in
-  let env = Modops.add_module mp mb env in
+  let env = Modops.add_module mb env in
   genv := add_digest env dp digest
 
 (* Check that the engagement expected by a library matches the initial one *)
@@ -66,16 +65,16 @@ let check_imports f caller env needed =
 
 
 (* Remove the body of opaque constants in modules *)
-(* also remove mod_expr ? *)
+(* also remove mod_expr ? Good idea!*)
 let rec lighten_module mb =
   { mb with
     mod_expr = Option.map lighten_modexpr mb.mod_expr;
-    mod_type = Option.map lighten_modexpr mb.mod_type }
+    mod_type = lighten_modexpr mb.mod_type }
 
 and lighten_struct struc =
   let lighten_body (l,body) = (l,match body with
     | SFBconst ({const_opaque=true} as x) -> SFBconst {x with const_body=None}
-    | (SFBconst _ | SFBmind _ | SFBalias _) as x -> x
+    | (SFBconst _ | SFBmind _ ) as x -> x
     | SFBmodule m -> SFBmodule (lighten_module m)
     | SFBmodtype m -> SFBmodtype
 	({m with
@@ -90,8 +89,8 @@ and lighten_modexpr = function
 			typ_expr = lighten_modexpr mty.typ_expr}),
 		  lighten_modexpr mexpr)
   | SEBident mp as x -> x
-  | SEBstruct (msid, struc) ->
-      SEBstruct (msid, lighten_struct struc)
+  | SEBstruct ( struc) ->
+      SEBstruct ( lighten_struct struc)
   | SEBapply (mexpr,marg,u) ->
       SEBapply (lighten_modexpr mexpr,lighten_modexpr marg,u)
   | SEBwith (seb,wdcl) ->
@@ -125,7 +124,7 @@ let import file (dp,mb,depends,engmt as vo) digest =
   let env = !genv in
   check_imports msg_warning dp env depends;
   check_engagement env engmt;
-  check_module (add_constraints mb.mod_constraints env) mb;
+  check_module (add_constraints mb.mod_constraints env) mb.mod_mp mb;
   stamp_library file digest;
   (* We drop proofs once checked *)
 (*  let mb = lighten_module mb in*)
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 88989b32e..ec1c908a6 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -32,7 +32,6 @@ type namedobject =
   | IndConstr of constructor * mutual_inductive_body
   | Module of module_body
   | Modtype of module_type_body
-  | Alias of module_path * struct_expr_body option
 
 (* adds above information about one mutual inductive: all types and
    constructors *)
@@ -60,13 +59,13 @@ let make_label_map mp list =
    match e with
     | SFBconst cb -> add_map (Constant cb)
     | SFBmind mib ->
-       add_nameobjects_of_mib (make_kn mp empty_dirpath l) mib map
+       add_nameobjects_of_mib (make_mind mp empty_dirpath l) mib map
     | SFBmodule mb -> add_map (Module mb)
     | SFBmodtype mtb -> add_map (Modtype mtb)
-    | SFBalias (mp,typ_opt,cst) -> add_map (Alias (mp,typ_opt))
   in
     List.fold_right add_one list Labmap.empty
 
+
 let check_conv_error error f env a1 a2 =
   try
     f env a1 a2
@@ -74,8 +73,8 @@ let check_conv_error error f env a1 a2 =
       NotConvertible -> error ()
 
 (* for now we do not allow reorderings *)
-let check_inductive env msid1 l info1 mib2 spec2 =
-  let kn = make_kn (MPself msid1) empty_dirpath l in
+let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2= 
+  let kn = make_mind  mp1 empty_dirpath l in
   let error () = error_not_match l spec2 in
   let check_conv f = check_conv_error error f in
   let mib1 =
@@ -83,6 +82,7 @@ let check_inductive env msid1 l info1 mib2 spec2 =
       | IndType ((_,0), mib) -> mib
       | _ -> error ()
   in
+  let mib2 =  subst_mind subst2 mib2 in
   let check_inductive_type env t1 t2 =
 
     (* Due to sort-polymorphism in inductive types, the conclusions of
@@ -155,7 +155,7 @@ let check_inductive env msid1 l info1 mib2 spec2 =
   (* the inductive types and constructors types have to be convertible *)
   check (fun mib -> mib.mind_nparams);
 
-  begin
+  (*begin
     match mib2.mind_equiv with
       | None -> ()
       | Some kn2' ->
@@ -165,7 +165,7 @@ let check_inductive env msid1 l info1 mib2 spec2 =
 	    | Some kn1' -> scrape_mind env kn1'
 	  in
 	    if kn1 <> kn2 then error ()
-  end;
+  end;*)
   (* we check that records and their field names are preserved. *)
   check (fun mib -> mib.mind_record);
   if mib1.mind_record then begin
@@ -187,7 +187,7 @@ let check_inductive env msid1 l info1 mib2 spec2 =
   let _ = array_map2_i check_cons_types mib1.mind_packets mib2.mind_packets
   in ()
 
-let check_constant env msid1 l info1 cb2 spec2 =
+let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
   let error () = error_not_match l spec2 in
   let check_conv f = check_conv_error error f in
   let check_type env t1 t2 =
@@ -236,30 +236,31 @@ let check_constant env msid1 l info1 cb2 spec2 =
         (t1,t2) in
     check_conv conv_leq env t1 t2
   in
-
-  match info1 with
-   | Constant cb1 ->
-      assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ;
-      (*Start by checking types*)
-      let typ1 = Typeops.type_of_constant_type env cb1.const_type in
-      let typ2 = Typeops.type_of_constant_type env cb2.const_type in
-      check_type env typ1 typ2;
-      let con = make_con (MPself msid1) empty_dirpath l in
-      (match cb2 with
-        | {const_body=Some lc2;const_opaque=false} ->
-	    let c2 = force_constr lc2 in
-	    let c1 = match cb1.const_body with
-	      | Some lc1 -> force_constr lc1
-	      | None -> Const con
-	    in
-	       check_conv conv env c1 c2
-        | _ -> ())
-   | IndType ((kn,i),mind1) ->
-      ignore (Util.error (
-       "The kernel does not recognize yet that a parameter can be " ^
-       "instantiated by an inductive type. Hint: you can rename the " ^
-       "inductive type and give a definition to map the old name to the new " ^
-       "name."));
+    match info1 with
+      | Constant cb1 ->
+	assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ;
+	  (*Start by checking types*)
+	  let cb1 = subst_const_body subst1 cb1 in
+	  let cb2 = subst_const_body subst2 cb2 in
+	  let typ1 = Typeops.type_of_constant_type env cb1.const_type in
+	  let typ2 = Typeops.type_of_constant_type env cb2.const_type in
+	    check_type env typ1 typ2;
+	  let con = make_con mp1 empty_dirpath l in
+	    (match cb2 with
+               | {const_body=Some lc2;const_opaque=false} ->
+		   let c2 = force_constr lc2 in
+		   let c1 = match cb1.const_body with
+		     | Some lc1 -> force_constr lc1
+		     | None -> Const con
+		   in
+		     check_conv conv env c1 c2
+               | _ -> ())
+      | IndType ((kn,i),mind1) ->
+	  ignore (Util.error (
+		    "The kernel does not recognize yet that a parameter can be " ^
+		      "instantiated by an inductive type. Hint: you can rename the " ^
+		      "inductive type and give a definition to map the old name to the new " ^
+		      "name."));
       assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ;
       if cb2.const_body <> None then error () ;
       let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in
@@ -278,57 +279,31 @@ let check_constant env msid1 l info1 cb2 spec2 =
        check_conv conv env ty1 ty2
    | _ -> error ()
 
-let rec check_modules env msid1 l msb1 msb2 =
-  let mp = (MPdot(MPself msid1,l)) in
-  let mty1 = module_type_of_module (Some mp) msb1 in
-  let mty2 =  module_type_of_module None msb2 in
-  check_modtypes env mty1 mty2 false
+let rec check_modules  env msb1 msb2 subst1 subst2 =
+  let mty1 = module_type_of_module env None msb1 in
+  let mty2 =  module_type_of_module env None msb2 in
+    check_modtypes env mty1 mty2 subst1 subst2 false;
+ 
 
-
-and check_signatures env (msid1,sig1) alias (msid2,sig2') =
-  let mp1 = MPself msid1 in
-  let env = add_signature mp1 sig1 env in
-  let alias = update_subst_alias alias (map_msid msid2 mp1) in
-  let sig2 = subst_structure alias sig2' in
-  let sig2 = subst_signature_msid msid2 mp1 sig2 in
+and check_signatures env mp1 sig1 sig2 subst1 subst2 = 
   let map1 = make_label_map mp1 sig1 in
-  let check_one_body (l,spec2) =
+  let check_one_body  (l,spec2) =
     let info1 =
       try
 	Labmap.find l map1
       with
-	  Not_found -> error_no_such_label_sub l msid1 msid2
+	  Not_found -> error_no_such_label_sub l mp1
     in
       match spec2 with
 	| SFBconst cb2 ->
-	    check_constant env msid1 l info1 cb2 spec2
+	    check_constant  env mp1 l info1 cb2 spec2 subst1 subst2
 	| SFBmind mib2 ->
-	    check_inductive env msid1 l info1 mib2 spec2
+	    check_inductive env mp1 l info1 mib2 spec2 subst1 subst2
 	| SFBmodule msb2 ->
 	    begin
 	      match info1 with
-		| Module msb -> check_modules env msid1 l msb msb2
-		| Alias (mp,typ_opt) ->let msb =
-		    {mod_expr = Some (SEBident mp);
-		     mod_type = typ_opt;
-		     mod_constraints = Constraint.empty;
-		     mod_alias = (lookup_modtype mp env).typ_alias;
-		     mod_retroknowledge = []} in
-		    check_modules env msid1 l msb msb2
-		| _ -> error_not_match l spec2
-	    end
-	| SFBalias (mp,typ_opt,_) ->
-	    begin
-	      match info1 with
-		| Alias (mp1,_) -> check_modpath_equiv env mp mp1
-		| Module msb ->
-		    let msb1 =
-		      {mod_expr = Some (SEBident mp);
-		       mod_type = typ_opt;
-		       mod_constraints = Constraint.empty;
-		       mod_alias = (lookup_modtype mp env).typ_alias;
-		       mod_retroknowledge = []} in
-			check_modules env msid1 l msb msb1
+		| Module msb -> check_modules env msb msb2 
+		    subst1 subst2
 		| _ -> error_not_match l spec2
 	    end
 	| SFBmodtype mtb2 ->
@@ -337,52 +312,61 @@ and check_signatures env (msid1,sig1) alias (msid2,sig2') =
 		| Modtype mtb -> mtb
 		| _ -> error_not_match l spec2
 	    in
-	      check_modtypes env mtb1 mtb2 true
+	    let env = add_module (module_body_of_type mtb2.typ_mp mtb2)
+	      (add_module (module_body_of_type mtb1.typ_mp mtb1) env) in
+	      check_modtypes  env mtb1 mtb2 subst1 subst2 true
   in
     List.iter check_one_body sig2
 
-and check_modtypes env mtb1 mtb2 equiv =
-  if mtb1==mtb2 then () else (* just in case  :) *)
-  let mtb1',mtb2'=
-    (match mtb1.typ_strength with
-	 None -> eval_struct env mtb1.typ_expr,
-	   eval_struct env mtb2.typ_expr
-       | Some mp -> strengthen  env mtb1.typ_expr mp,
-	   eval_struct env mtb2.typ_expr) in
-      let rec check_structure env str1 str2 equiv =
-	match str1, str2 with
-	  | SEBstruct (msid1,list1),
-	    SEBstruct (msid2,list2) ->
-	      check_signatures env
-		(msid1,list1) mtb1.typ_alias (msid2,list2);
-	      if equiv then
-		check_signatures env
-		  (msid2,list2) mtb2.typ_alias  (msid1,list1)
+and check_modtypes  env mtb1 mtb2 subst1 subst2 equiv = 
+  if mtb1==mtb2 then () else 
+  let mtb1',mtb2'=mtb1.typ_expr,mtb2.typ_expr in
+  let rec check_structure  env str1 str2 equiv subst1 subst2 = 
+	match str1,str2 with
+	  | SEBstruct (list1), 
+	    SEBstruct (list2) -> 
+	       check_signatures env
+		mtb1.typ_mp list1 list2 subst1 subst2;
+		if equiv then
+		  check_signatures  env 
+		     mtb2.typ_mp list2 list1 subst1 subst2
+		else
+		  ()
 	  | SEBfunctor (arg_id1,arg_t1,body_t1),
 	      SEBfunctor (arg_id2,arg_t2,body_t2) ->
-	      check_modtypes env arg_t2 arg_t1 equiv;
+	       check_modtypes env 
+		arg_t2 arg_t1
+		(map_mp arg_t1.typ_mp arg_t2.typ_mp) subst2
+		equiv ;
 		(* contravariant *)
-	      let env =
-		add_module (MPbound arg_id2) (module_body_of_type arg_t2) env
+	      let env = add_module 
+		(module_body_of_type (MPbound arg_id2) arg_t2) env 
 	      in
-	      let body_t1' =
-		(* since we are just checking well-typedness we do not need
-		   to expand any constant. Hence the identity resolver. *)
-		subst_struct_expr
-		  (map_mbid arg_id1 (MPbound arg_id2))
-		  body_t1
+	      let env = match body_t1 with
+		  SEBstruct str -> 
+		    add_module {mod_mp = mtb1.typ_mp;
+				mod_expr = None;
+				mod_type = body_t1;
+				mod_type_alg= None;
+				mod_constraints=mtb1.typ_constraints;
+				mod_retroknowledge = [];
+				mod_delta = mtb1.typ_delta} env
+		| _ -> env
 	      in
-		check_structure env (eval_struct env body_t1')
-		  (eval_struct env body_t2) equiv
+		check_structure env body_t1 body_t2 equiv 
+		  (join (map_mbid arg_id1 (MPbound arg_id2)) subst1)
+		  subst2
 	  | _ , _ -> error_incompatible_modtypes mtb1 mtb2
       in
      if mtb1'== mtb2' then ()
-     else check_structure env mtb1' mtb2' equiv
+     else check_structure  env mtb1' mtb2' equiv subst1 subst2
 
 let check_subtypes env sup super =
   (*if sup<>super then*)
-  check_modtypes env sup super false
+  check_modtypes env (strengthen env sup sup.typ_mp) super empty_subst 
+    (map_mp super.typ_mp sup.typ_mp) false 
 
 let check_equal env sup super =
   (*if sup<>super then*)
-  check_modtypes env sup super true
+  check_modtypes env sup super empty_subst 
+    (map_mp super.typ_mp sup.typ_mp) true
diff --git a/checker/term.ml b/checker/term.ml
index 92d898b31..658eac4f0 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -489,7 +489,7 @@ let compare_constr f t1 t2 =
           f h1 h2 & List.for_all2 f l1 l2
         else false
   | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & array_for_all2 f l1 l2
-  | Const c1, Const c2 -> c1 = c2
+  | Const c1, Const c2 -> eq_constant c1 c2
   | Ind c1, Ind c2 -> c1 = c2
   | Construct c1, Construct c2 -> c1 = c2
   | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 3a4f2f825..e5cf6a6d6 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -228,7 +228,7 @@ let judge_of_inductive_knowing_parameters env ind (paramstyp:constr array) =
   let (mib,mip) =
     try lookup_mind_specif env ind
     with Not_found ->
-      failwith ("Cannot find inductive: "^string_of_kn (fst ind)) in
+      failwith ("Cannot find inductive: "^string_of_mind (fst ind)) in
   check_args env c mib.mind_hyps;
   type_of_inductive_knowing_parameters env mip paramstyp
 
@@ -244,7 +244,7 @@ let judge_of_constructor env c =
     let mib =
       try lookup_mind kn env
       with Not_found ->
-        failwith ("Cannot find inductive: "^string_of_kn (fst (fst c))) in
+        failwith ("Cannot find inductive: "^string_of_mind (fst (fst c))) in
     check_args env constr mib.mind_hyps in
   let specif = lookup_mind_specif env (inductive_of_constructor c) in
   type_of_constructor c specif