Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 316 insertions, 488 deletions

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index ab8b60be..314cc0ee 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -1,305 +1,249 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: mod_subst.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* Created by Claudio Sacerdoti from contents of term.ml, names.ml and
+   new support for constant inlining in functor application, Nov 2004 *)
+(* Optimizations and bug fixes by Élie Soubiran, from Feb 2008 *)
+
+(* This file provides types and functions for managing name
+   substitution in module constructions *)
 
 open Pp
 open Util
 open Names
 open Term
 
+(* For Inline, the int is an inlining level, and the constr (if present)
+   is the term into which we should inline *)
 
 type delta_hint =
-    Inline of constr option
+  | Inline of int * constr option
   | Equiv of kernel_name
-  | Prefix_equiv of module_path
 
-type delta_key = 
-    KN of kernel_name
-  | MP of module_path
+(* NB: earlier constructor Prefix_equiv of module_path
+   is now stored in a separate table, see Deltamap.t below *)
+
+module Deltamap = struct
+  type t = module_path MPmap.t * delta_hint KNmap.t
+  let empty = MPmap.empty, KNmap.empty
+  let add_kn kn hint (mm,km) = (mm,KNmap.add kn hint km)
+  let add_mp mp mp' (mm,km) = (MPmap.add mp mp' mm, km)
+  let find_mp mp map = MPmap.find mp (fst map)
+  let find_kn kn map = KNmap.find kn (snd map)
+  let mem_mp mp map = MPmap.mem mp (fst map)
+  let mem_kn kn map = KNmap.mem kn (snd map)
+  let fold_kn f map i = KNmap.fold f (snd map) i
+  let fold fmp fkn (mm,km) i =
+    MPmap.fold fmp mm (KNmap.fold fkn km i)
+  let join map1 map2 = fold add_mp add_kn map1 map2
+end
+
+type delta_resolver = Deltamap.t
 
-module Deltamap =  Map.Make(struct 
-			      type t = delta_key
-			      let compare = Pervasives.compare
-			    end)
+let empty_delta_resolver = Deltamap.empty
 
-type delta_resolver = delta_hint Deltamap.t
+module MBImap = Map.Make
+  (struct
+    type t = mod_bound_id
+    let compare = Pervasives.compare
+   end)
+
+module Umap = struct
+  type 'a t = 'a MPmap.t * 'a MBImap.t
+  let empty = MPmap.empty, MBImap.empty
+  let is_empty (m1,m2) = MPmap.is_empty m1 && MBImap.is_empty m2
+  let add_mbi mbi x (m1,m2) = (m1,MBImap.add mbi x m2)
+  let add_mp mp x (m1,m2) = (MPmap.add mp x m1, m2)
+  let find_mp mp map = MPmap.find mp (fst map)
+  let find_mbi mbi map = MBImap.find mbi (snd map)
+  let mem_mp mp map = MPmap.mem mp (fst map)
+  let mem_mbi mbi map = MBImap.mem mbi (snd map)
+  let iter_mbi f map = MBImap.iter f (snd map)
+  let fold fmp fmbi (m1,m2) i =
+    MPmap.fold fmp m1 (MBImap.fold fmbi m2 i)
+  let join map1 map2 = fold add_mp add_mbi map1 map2
+end
 
-let empty_delta_resolver = Deltamap.empty
+type substitution = (module_path * delta_resolver) Umap.t
 
-type substitution_domain = 
-  | MBI of mod_bound_id
-  | MPI of module_path
+let empty_subst = Umap.empty
 
-let string_of_subst_domain = function
- | MBI mbid -> debug_string_of_mbid mbid
- | MPI mp -> string_of_mp mp
+let is_empty_subst = Umap.is_empty
 
-module Umap = Map.Make(struct
-			 type t = substitution_domain
-			 let compare = Pervasives.compare
-		       end)
+(* <debug> *)
 
-type substitution = (module_path * delta_resolver) Umap.t
-    
-let empty_subst = Umap.empty
+let string_of_hint = function
+  | Inline (_,Some _) -> "inline(Some _)"
+  | Inline _ -> "inline()"
+  | Equiv kn -> string_of_kn kn
+
+let debug_string_of_delta resolve =
+  let kn_to_string kn hint s =
+    s^", "^(string_of_kn kn)^"=>"^(string_of_hint hint)
+  in
+  let mp_to_string mp mp' s =
+    s^", "^(string_of_mp mp)^"=>"^(string_of_mp mp')
+  in
+  Deltamap.fold mp_to_string kn_to_string resolve ""
+
+let list_contents sub =
+  let one_pair (mp,reso) = (string_of_mp mp,debug_string_of_delta reso) in
+  let mp_one_pair mp0 p l = (string_of_mp mp0, one_pair p)::l in
+  let mbi_one_pair mbi p l = (debug_string_of_mbid mbi, one_pair p)::l in
+  Umap.fold mp_one_pair mbi_one_pair sub []
+
+let debug_string_of_subst sub =
+  let l = List.map (fun (s1,(s2,s3)) -> s1^"|->"^s2^"["^s3^"]")
+    (list_contents sub)
+  in
+  "{" ^ String.concat "; " l ^ "}"
+
+let debug_pr_delta resolve =
+  str (debug_string_of_delta resolve)
+
+let debug_pr_subst sub =
+  let l = list_contents sub in
+  let f (s1,(s2,s3)) = hov 2 (str s1 ++ spc () ++ str "|-> " ++ str s2 ++
+			      spc () ++ str "[" ++ str s3 ++ str "]")
+  in
+  str "{" ++ hov 2 (prlist_with_sep pr_comma f l) ++ str "}"
 
+(* </debug> *)
 
-let string_of_subst_domain = function
-  | MBI mbid -> debug_string_of_mbid mbid
-  | MPI mp -> string_of_mp mp
-      
-let add_mbid mbid mp resolve =
-  Umap.add (MBI mbid) (mp,resolve)
-let add_mp mp1 mp2 resolve =
-  Umap.add (MPI mp1) (mp2,resolve)
+(** Extending a [delta_resolver] *)
 
+let add_inline_delta_resolver kn (lev,oc) = Deltamap.add_kn kn (Inline (lev,oc))
+
+let add_kn_delta_resolver kn kn' = Deltamap.add_kn kn (Equiv kn')
+
+let add_mp_delta_resolver mp1 mp2 = Deltamap.add_mp mp1 mp2
+
+(** Extending a [substitution *)
+
+let add_mbid mbid mp resolve s = Umap.add_mbi mbid (mp,resolve) s
+let add_mp mp1 mp2 resolve s = Umap.add_mp mp1 (mp2,resolve) s
 
 let map_mbid mbid mp resolve = add_mbid mbid mp resolve empty_subst
 let map_mp mp1 mp2 resolve = add_mp mp1 mp2 resolve 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 mp_in_delta mp = Deltamap.mem_mp mp
 
-let remove_mp_delta_resolver resolver mp =
-    Deltamap.remove (MP mp) resolver
+let kn_in_delta kn resolver =
+  try
+    match Deltamap.find_kn kn resolver with
+      | Equiv _ -> true
+      | Inline _ -> false
+  with Not_found -> false
 
-exception Inline_kn
+let con_in_delta con resolver = kn_in_delta (user_con con) resolver
+let mind_in_delta mind resolver = kn_in_delta (user_mind mind) resolver
 
-let rec find_prefix resolve mp = 
+let mp_of_delta resolve mp =
+ try Deltamap.find_mp mp resolve with Not_found -> mp
+
+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"	
+    | MPdot(mp,l) as mp_sup ->
+	(try Deltamap.find_mp mp_sup resolve
+	 with Not_found -> MPdot(sub_mp mp,l))
+    | p -> Deltamap.find_mp p resolve
   in
-    try 
-      sub_mp mp
-    with
-	Not_found -> mp
+  try sub_mp mp with Not_found -> mp
 
-exception Change_equiv_to_inline of constr
+exception Change_equiv_to_inline of (int * constr)
 
 let solve_delta_kn resolve kn =
-  try 
-      match Deltamap.find (KN kn) resolve with
-	| Equiv kn1 -> kn1
-	| Inline (Some c) -> 
-	    raise (Change_equiv_to_inline c)
-	| Inline None -> 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
-	      
+  try
+    match Deltamap.find_kn kn resolve with
+      | Equiv kn1 -> kn1
+      | Inline (lev, Some c) ->	raise (Change_equiv_to_inline (lev,c))
+      | Inline (_, None) -> raise Not_found
+  with Not_found ->
+    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 kn_of_delta resolve kn =
+  try solve_delta_kn resolve kn
+  with _ -> kn
+
+let constant_of_delta_kn resolve kn =
+  constant_of_kn_equiv kn (kn_of_delta resolve kn)
+
+let gen_of_delta resolve x kn fix_can =
+  try
+    let new_kn = solve_delta_kn resolve kn in
+    if kn == new_kn then x else fix_can new_kn
+  with _ -> x
 
 let constant_of_delta resolve con =
   let kn = user_con con in
-    try 
-      let new_kn = solve_delta_kn resolve kn in
-	if kn == new_kn then
-	  con
-	else
-	  constant_of_kn_equiv kn new_kn
-    with 
-	_ -> con 
-	
+  gen_of_delta resolve con kn (constant_of_kn_equiv kn)
+
 let constant_of_delta2 resolve con =
-  let kn = canonical_con con in
-  let kn1 = user_con con in
-    try 
-      let new_kn = solve_delta_kn resolve kn in
-	if kn == new_kn then
-	  con
-	else
-	  constant_of_kn_equiv kn1 new_kn
-    with 
-	_ -> con
+  let kn, kn' = canonical_con con, user_con con in
+  gen_of_delta resolve con kn (constant_of_kn_equiv kn')
+
+let mind_of_delta_kn resolve kn =
+  mind_of_kn_equiv kn (kn_of_delta resolve kn)
 
 let mind_of_delta resolve mind =
   let kn = user_mind mind in
-    try
-      let new_kn = solve_delta_kn resolve kn in
-	if kn == new_kn then
-	  mind
-	else
-	  mind_of_kn_equiv kn new_kn
-    with 
-	_ -> mind 
+  gen_of_delta resolve mind kn (mind_of_kn_equiv kn)
 
 let mind_of_delta2 resolve mind =
-  let kn = canonical_mind mind in
-  let kn1 = user_mind mind in
-    try
-      let new_kn = solve_delta_kn resolve kn in
-	if kn == new_kn then
-	  mind
-	else
-	  mind_of_kn_equiv kn1 new_kn
-    with 
-	_ -> mind
-	  
-
-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 []
+  let kn, kn' = canonical_mind mind, user_mind mind in
+  gen_of_delta resolve mind kn (mind_of_kn_equiv kn')
+
+let inline_of_delta inline resolver =
+  match inline with
+    | None -> []
+    | Some inl_lev ->
+      let extract kn hint l =
+	match hint with
+	  | Inline (lev,_) -> if lev <= inl_lev then (lev,kn)::l else l
+	  | _ -> l
+      in
+      Deltamap.fold_kn extract resolver []
+
+let find_inline_of_delta kn resolve =
+  match Deltamap.find_kn kn resolve with
+    | Inline (_,o) -> o
+    | _ -> raise Not_found
 
-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 string_of_key = function
-      | KN kn -> string_of_kn kn
-      | MP mp -> string_of_mp mp
+  try find_inline_of_delta kn2 resolve
+  with Not_found ->
+    try find_inline_of_delta kn1 resolve
+    with Not_found -> None
 
-let string_of_hint = function
-      | Inline _ -> "inline"
-      | Equiv kn -> string_of_kn kn
-      | Prefix_equiv mp -> string_of_mp mp
-
-let debug_string_of_delta resolve =
-  let to_string key hint s = 
-    s^", "^(string_of_key key)^"=>"^(string_of_hint hint)
-  in 
-    Deltamap.fold to_string resolve ""  
-      
-let list_contents sub = 
-  let one_pair uid (mp,reso) l =
-    (string_of_subst_domain uid, string_of_mp mp,debug_string_of_delta reso)::l
-  in
-    Umap.fold one_pair sub []
-      
-let debug_string_of_subst sub =
-  let l = List.map (fun (s1,s2,s3) -> s1^"|->"^s2^"["^s3^"]")
-    (list_contents sub) in
-    "{" ^ String.concat "; " l ^ "}"
-      
-let debug_pr_delta resolve = 
-  str (debug_string_of_delta resolve)
-
-let debug_pr_subst sub =
-  let l = list_contents sub in
-  let f (s1,s2,s3) = hov 2 (str s1 ++ spc () ++ str "|-> " ++ str s2 ++
-			      spc () ++ str "[" ++ str s3 ++ str "]") 
-  in
-    str "{" ++ hov 2 (prlist_with_sep pr_comma f l) ++ str "}"
-      
-      
 let subst_mp0 sub mp = (* 's like subst *)
  let rec aux mp =
   match mp with
-    | MPfile sid -> 
-        let mp',resolve = Umap.find (MPI (MPfile sid)) sub in
-         mp',resolve
+    | MPfile sid -> Umap.find_mp mp sub
     | MPbound bid ->
 	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
+	  try Umap.find_mbi bid sub
+	  with Not_found -> Umap.find_mp mp sub
 	end
     | MPdot (mp1,l) as mp2 ->
 	begin
-	  try
-	    let mp',resolve = Umap.find (MPI mp2) sub in
-              mp',resolve
+	  try Umap.find_mp mp2 sub
 	  with Not_found ->
 	    let mp1',resolve = aux mp1 in
-	      MPdot (mp1',l),resolve
+	    MPdot (mp1',l),resolve
 	end
  in
-  try
-    Some (aux mp)
-  with Not_found -> None
+ try Some (aux mp) with Not_found -> None
 
 let subst_mp sub mp =
  match subst_mp0 sub mp with
@@ -327,107 +271,47 @@ 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 gen_subst_mp f sub mp1 mp2 =
+  match subst_mp0 sub mp1, subst_mp0 sub mp2 with
+    | None, None -> raise No_subst
+    | Some (mp',resolve), None -> User, (f mp' mp2), resolve
+    | None, Some (mp',resolve) -> Canonical, (f mp1 mp'), resolve
+    | Some (mp1',_), Some (mp2',resolve2) -> Canonical, (f mp1' mp2'), resolve2
 
-let subst_con sub con =
-  let kn1,kn2 = user_con con,canonical_con con in
+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,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,mkConst con
-	      |Canonical ->
-		  let con = constant_of_delta2 resolve con' in
-		con,mkConst con
-	    end
-	  | Some t ->
-	    (* In case of inlining, discard the canonical part (cf #2608) *)
-	    constant_of_kn (user_con con'), t
-    with No_subst -> con , mkConst con 
- 
+  let rebuild_mind mp1 mp2 = make_mind_equiv mp1 mp2 dir l in
+  try
+    let side,mind',resolve = gen_subst_mp rebuild_mind sub mp1 mp2 in
+    match side with
+      | User -> mind_of_delta resolve mind'
+      | Canonical -> mind_of_delta2 resolve mind'
+  with No_subst -> mind
 
 let subst_con0 sub 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 
+  let rebuild_con mp1 mp2 = make_con_equiv mp1 mp2 dir l in
+  let dup con = con, mkConst con in
+  let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in
+  match constant_of_delta_with_inline resolve con' with
+    | Some t ->
+      (* In case of inlining, discard the canonical part (cf #2608) *)
+      constant_of_kn (user_con con'), t
+    | None ->
+      let con'' = match side with
+	| User -> constant_of_delta resolve con'
+	| Canonical -> constant_of_delta2 resolve con'
       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 (mkConst con)
-	      |Canonical ->
-		  let con = constant_of_delta2 resolve con' in
-		Some (mkConst con)
-	    end
-	  | t ->  t
-    with No_subst -> Some (mkConst con) 
-		
+      if con'' == con then raise No_subst else dup con''
+
+let subst_con sub con =
+  try subst_con0 sub con
+  with No_subst -> con, mkConst con
+
 (* Here the semantics is completely unclear.
    What does "Hint Unfold t" means when "t" is a parameter?
    Does the user mean "Unfold X.t" or does she mean "Unfold y"
@@ -437,29 +321,22 @@ let subst_evaluable_reference subst = function
   | EvalVarRef id -> EvalVarRef id
   | EvalConstRef kn -> EvalConstRef (fst (subst_con subst kn))
 
-
-
 let rec map_kn f f' c =
   let func = map_kn f f' in
     match kind_of_term c with
-      | Const kn ->
-	  (match f' kn with
-	       None -> c
-	     | Some const ->const)
+      | Const kn -> (try snd (f' kn) with No_subst -> c)
       | Ind (kn,i) ->
-         (match f kn with
-             None -> c
-           | Some kn' ->
-	      mkInd (kn',i))
+	  let kn' = f kn in
+	  if kn'==kn then c else mkInd (kn',i)
       | Construct ((kn,i),j) ->
-         (match f kn with
-             None -> c
-           | Some kn' ->
-	       mkConstruct ((kn',i),j))
+	  let kn' = f kn in
+	  if kn'==kn then c else mkConstruct ((kn',i),j)
       | Case (ci,p,ct,l) ->
 	  let ci_ind =
             let (kn,i) = ci.ci_ind in
-              (match f kn with None -> ci.ci_ind | Some kn' -> kn',i ) in
+	    let kn' = f kn in
+	    if kn'==kn then ci.ci_ind else kn',i
+	  in
 	  let p' = func p in
 	  let ct' = func ct in
 	  let l' = array_smartmap func l in
@@ -510,8 +387,9 @@ let rec map_kn f f' c =
 	    else mkCoFix (ln,(lna,tl',bl'))
       | _ -> c
 
-let subst_mps sub =
-  map_kn (subst_mind0 sub) (subst_con0 sub)
+let subst_mps sub c =
+  if is_empty_subst sub then c
+  else map_kn (subst_ind sub) (subst_con0 sub) c
 
 let rec replace_mp_in_mp mpfrom mpto mp =
   match mp with
@@ -533,117 +411,76 @@ let rec mp_in_mp mp mp1 =
     | _ when mp1 = mp -> true
     | MPdot (mp2,l) -> mp_in_mp mp mp2
     | _ -> false
-	
-let mp_in_key mp key = 
-  match key with
-    | MP mp1 -> 
-	mp_in_mp mp mp1
-    | KN kn -> 
-	let mp1,dir,l = repr_kn kn in
-	  mp_in_mp mp mp1
-	    
+
 let subset_prefixed_by mp resolver =
-  let prefixmp key hint resolv =
-    match hint with 
-      | Inline _ -> resolv
-      | _ ->
-	  if mp_in_key mp key then
-	    Deltamap.add key hint resolv
-	  else 
-	    resolv
+  let mp_prefix mkey mequ rslv =
+    if mp_in_mp mp mkey then Deltamap.add_mp mkey mequ rslv else rslv
+  in
+  let kn_prefix kn hint rslv =
+    match hint with
+      | Inline _ -> rslv
+      | Equiv _ ->
+	if mp_in_mp mp (modpath kn) then Deltamap.add_kn kn hint rslv else rslv
   in
-    Deltamap.fold prefixmp resolver empty_delta_resolver
+  Deltamap.fold mp_prefix kn_prefix 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
+  let mp_apply_subst mkey mequ rslv =
+    Deltamap.add_mp (subst_mp subst mkey) mequ rslv
+  in
+  let kn_apply_subst kkey hint rslv =
+    Deltamap.add_kn (subst_kn subst kkey) hint rslv
   in
-    Deltamap.fold apply_subst resolver empty_delta_resolver
+  Deltamap.fold mp_apply_subst kn_apply_subst resolver empty_delta_resolver
 
-let subst_mp_delta sub mp key=
+let subst_mp_delta sub mp mkey =
  match subst_mp0 sub mp with
     None -> empty_delta_resolver,mp
-  | Some (mp',resolve) -> 
+  | 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 empty_delta_resolver) 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) ->
-	  (try
-	     Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver
-	   with
-	       Change_equiv_to_inline c ->
-		 Deltamap.add key (Inline (Some c)) resolver)
-      | Inline None ->
-	  Deltamap.add key hint resolver
-      | Inline (Some t) ->
-	  Deltamap.add key (Inline (Some (subst_mps subst t))) resolver
+      (subst_dom_delta_resolver
+	 (map_mp mp1 mkey empty_delta_resolver) resolve1),mp1
+
+let gen_subst_delta_resolver dom subst resolver =
+  let mp_apply_subst mkey mequ rslv =
+    let mkey' = if dom then subst_mp subst mkey else mkey in
+    let rslv',mequ' = subst_mp_delta subst mequ mkey in
+    Deltamap.join rslv' (Deltamap.add_mp mkey' mequ' rslv)
   in
-    Deltamap.fold apply_subst resolver empty_delta_resolver
-
-let subst_dom_codom_delta_resolver subst resolver =
-  let apply_subst key hint resolver =
-    match key,hint with
-	(MP mp1),Prefix_equiv mp ->
-	  let key = MP (subst_mp subst mp1) in
-	  let derived_resolve,mpnew = subst_mp_delta subst mp key in
-	    Deltamap.fold Deltamap.add derived_resolve
-	      (Deltamap.add key (Prefix_equiv mpnew) resolver)
-      | (KN kn1),(Equiv kn) ->
-	  let key = KN (subst_kn subst kn1) in
-	    (try
-	       Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver
-	     with
-		 Change_equiv_to_inline c ->
-		   Deltamap.add key (Inline (Some c)) resolver)
-      | (KN kn),Inline None ->
-	  let key = KN (subst_kn subst kn) in
-	    Deltamap.add key hint resolver
-      | (KN kn),Inline (Some t) ->
-	  let key = KN (subst_kn subst kn) in
-	  Deltamap.add key (Inline (Some (subst_mps subst t))) resolver
-      | _,_ -> anomaly "Mod_subst: Bad association in resolver" 
+  let kn_apply_subst kkey hint rslv =
+    let kkey' = if dom then subst_kn subst kkey else kkey in
+    let hint' = match hint with
+      | Equiv kequ ->
+	  (try Equiv (subst_kn_delta subst kequ)
+	   with Change_equiv_to_inline (lev,c) -> Inline (lev,Some c))
+      | Inline (lev,Some t) -> Inline (lev,Some (subst_mps subst t))
+      | Inline (_,None) -> hint
+    in
+    Deltamap.add_kn kkey' hint' rslv
   in
-    Deltamap.fold apply_subst resolver empty_delta_resolver
+  Deltamap.fold mp_apply_subst kn_apply_subst resolver empty_delta_resolver
+
+let subst_codom_delta_resolver = gen_subst_delta_resolver false
+let subst_dom_codom_delta_resolver = gen_subst_delta_resolver true
 
 let update_delta_resolver resolver1 resolver2 =
- let apply_res key hint res = 
-      try
-	if Deltamap.mem key resolver2 then
-	  res else
-	match hint with
-	    Prefix_equiv mp ->
-	      let new_hint =
-		Prefix_equiv (find_prefix resolver2 mp)
-	      in Deltamap.add key new_hint res
-	  | Equiv kn ->
-	      (try 
-		 let new_hint =
-		   Equiv (solve_delta_kn resolver2 kn)
-		 in Deltamap.add key new_hint res
-	       with
-		   Change_equiv_to_inline c ->
-		     Deltamap.add key (Inline (Some c)) res)
-	  | _ -> Deltamap.add key hint res
-      with Not_found ->
-	Deltamap.add key hint res
-    in
-      Deltamap.fold apply_res resolver1 empty_delta_resolver
+  let mp_apply_rslv mkey mequ rslv =
+    if Deltamap.mem_mp mkey resolver2 then rslv
+    else Deltamap.add_mp mkey (find_prefix resolver2 mequ) rslv
+  in
+  let kn_apply_rslv kkey hint rslv =
+    if Deltamap.mem_kn kkey resolver2 then rslv
+    else
+      let hint' = match hint with
+	| Equiv kequ ->
+	  (try Equiv (solve_delta_kn resolver2 kequ)
+	   with Change_equiv_to_inline (lev,c) -> Inline (lev, Some c))
+	| _ -> hint
+      in
+      Deltamap.add_kn kkey hint' rslv
+  in
+  Deltamap.fold mp_apply_rslv kn_apply_rslv resolver1 empty_delta_resolver
 
 let add_delta_resolver resolver1 resolver2 =
   if resolver1 == resolver2 then
@@ -651,63 +488,54 @@ let add_delta_resolver resolver1 resolver2 =
   else if resolver2 = empty_delta_resolver then
     resolver1
   else
-    Deltamap.fold Deltamap.add (update_delta_resolver resolver1 resolver2)
-      resolver2
+    Deltamap.join (update_delta_resolver resolver1 resolver2) resolver2
 
 let substition_prefixed_by k mp subst =
-  let prefixmp key (mp_to,reso) sub =
-    match key with 
-      | MPI mpk ->
-	  if mp_in_mp mp mpk && mp <> mpk then
-	    let new_key = replace_mp_in_mp mp k mpk in
-	      Umap.add (MPI new_key) (mp_to,reso) sub
-	  else 
-	    sub
-      |  _ -> sub
+  let mp_prefixmp kmp (mp_to,reso) sub =
+    if mp_in_mp mp kmp && mp <> kmp then
+      let new_key = replace_mp_in_mp mp k kmp in
+      Umap.add_mp new_key (mp_to,reso) sub
+    else sub
+  in
+  let mbi_prefixmp mbi _ sub = sub
   in
-    Umap.fold prefixmp subst empty_subst
+  Umap.fold mp_prefixmp mbi_prefixmp subst empty_subst
 
-let join (subst1 : substitution) (subst2 : substitution) =
-  let apply_subst key (mp,resolve) res =
+let join subst1 subst2 =
+  let apply_subst mpk add (mp,resolve) res =
     let mp',resolve' =
       match subst_mp0 subst2 mp with
-	  None -> mp, None
-	| Some (mp',resolve') ->  mp'
-	    ,Some resolve' in
-    let resolve'' : delta_resolver =
+	| None -> mp, None
+	| Some (mp',resolve') ->  mp', Some resolve' in
+    let resolve'' =
       match resolve' with
-          Some res -> 
-	    add_delta_resolver 
+        | Some res ->
+	    add_delta_resolver
 	      (subst_dom_codom_delta_resolver subst2 resolve) res
-	| None -> 
+	| None ->
 	    subst_codom_delta_resolver subst2 resolve
     in
-    let k = match key with MBI mp -> MPbound mp | MPI mp -> mp in
-    let prefixed_subst = substition_prefixed_by k mp subst2 in
-      Umap.fold Umap.add prefixed_subst 
-	(Umap.add key (mp',resolve'') res) in
-  let subst = Umap.fold apply_subst subst1 empty_subst in
-    (Umap.fold Umap.add subst2 subst)   
-
-
-
-let rec occur_in_path uid path =
- match uid,path with
-  | MBI bid,MPbound bid' -> bid = bid'
-  | _,MPdot (mp1,_) -> occur_in_path uid mp1
+    let prefixed_subst = substition_prefixed_by mpk mp' subst2 in
+    Umap.join prefixed_subst (add (mp',resolve'') res)
+  in
+  let mp_apply_subst mp = apply_subst mp (Umap.add_mp mp) in
+  let mbi_apply_subst mbi = apply_subst (MPbound mbi) (Umap.add_mbi mbi) in
+  let subst = Umap.fold mp_apply_subst mbi_apply_subst subst1 empty_subst in
+  Umap.join subst2 subst
+
+let rec occur_in_path mbi = function
+  | MPbound bid' -> mbi = bid'
+  | MPdot (mp1,_) -> occur_in_path mbi mp1
   | _ -> false
 
-let occur_uid uid sub =
-  let check_one uid' (mp,_) =
-    if uid = uid' || occur_in_path uid mp then raise Exit
+let occur_mbid mbi sub =
+  let check_one mbi' (mp,_) =
+    if mbi = mbi' || occur_in_path mbi mp then raise Exit
   in
-    try
-      Umap.iter check_one sub;
-      false
-    with Exit -> true
-
-
-let occur_mbid uid = occur_uid (MBI uid)
+  try
+    Umap.iter_mbi check_one sub;
+    false
+  with Exit -> true
 
 type 'a lazy_subst =
   | LSval of 'a