1 files changed, 21 insertions, 21 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 324f883e8e..a1cb0ec68e 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -8,10 +8,11 @@
 
 open Pp
 open CErrors
+open Sorts
 open Util
 open Names
 open Nameops
-open Term
+open Constr
 open Vars
 open Environ
 
@@ -124,10 +125,9 @@ end
 
 (* The type of mappings for existential variables *)
 
-module Dummy = struct end
-module Store = Store.Make(Dummy)
+module Store = Store.Make ()
 
-type evar = Term.existential_key
+type evar = existential_key
 
 let string_of_existential evk = "?X" ^ string_of_int (Evar.repr evk)
 
@@ -243,7 +243,7 @@ let evar_instance_array test_id info args =
     instrec filter (evar_context info) 0
 
 let make_evar_instance_array info args =
-  evar_instance_array (NamedDecl.get_id %> isVarId) info args
+  evar_instance_array (NamedDecl.get_id %> Term.isVarId) info args
 
 let instantiate_evar_array info c args =
   let inst = make_evar_instance_array info args in
@@ -281,9 +281,9 @@ type 'a freelisted = {
 (* Collects all metavars appearing in a constr *)
 let metavars_of c =
   let rec collrec acc c =
-    match kind_of_term c with
+    match kind c with
       | Meta mv -> Int.Set.add mv acc
-      | _         -> Term.fold_constr collrec acc c
+      | _         -> Constr.fold collrec acc c
   in
   collrec Int.Set.empty c
 
@@ -371,17 +371,17 @@ val key : Id.t -> t -> Evar.t
 end =
 struct
 
-type t = Id.t EvMap.t * existential_key Idmap.t
+type t = Id.t EvMap.t * existential_key Id.Map.t
 
-let empty = (EvMap.empty, Idmap.empty)
+let empty = (EvMap.empty, Id.Map.empty)
 
 let add_name_newly_undefined id evk evi (evtoid, idtoev as names) =
   match id with
   | None -> names
   | Some id ->
-    if Idmap.mem id idtoev then
+    if Id.Map.mem id idtoev then
       user_err  (str "Already an existential evar of name " ++ pr_id id);
-    (EvMap.add evk id evtoid, Idmap.add id evk idtoev)
+    (EvMap.add evk id evtoid, Id.Map.add id evk idtoev)
 
 let add_name_undefined naming evk evi (evtoid,idtoev as evar_names) =
   if EvMap.mem evk evtoid then
@@ -393,15 +393,15 @@ let remove_name_defined evk (evtoid, idtoev as names) =
   let id = try Some (EvMap.find evk evtoid) with Not_found -> None in
   match id with
   | None -> names
-  | Some id -> (EvMap.remove evk evtoid, Idmap.remove id idtoev)
+  | Some id -> (EvMap.remove evk evtoid, Id.Map.remove id idtoev)
 
 let rename evk id (evtoid, idtoev) =
   let id' = try Some (EvMap.find evk evtoid) with Not_found -> None in
   match id' with
-  | None -> (EvMap.add evk id evtoid, Idmap.add id evk idtoev)
+  | None -> (EvMap.add evk id evtoid, Id.Map.add id evk idtoev)
   | Some id' ->
-    if Idmap.mem id idtoev then anomaly (str "Evar name already in use.");
-    (EvMap.update evk id evtoid (* overwrite old name *), Idmap.add id evk (Idmap.remove id' idtoev))
+    if Id.Map.mem id idtoev then anomaly (str "Evar name already in use.");
+    (EvMap.update evk id evtoid (* overwrite old name *), Id.Map.add id evk (Id.Map.remove id' idtoev))
 
 let reassign_name_defined evk evk' (evtoid, idtoev as names) =
   let id = try Some (EvMap.find evk evtoid) with Not_found -> None in
@@ -409,13 +409,13 @@ let reassign_name_defined evk evk' (evtoid, idtoev as names) =
   | None -> names (** evk' must not be defined *)
   | Some id ->
     (EvMap.add evk' id (EvMap.remove evk evtoid),
-    Idmap.add id evk' (Idmap.remove id idtoev))
+    Id.Map.add id evk' (Id.Map.remove id idtoev))
 
 let ident evk (evtoid, _) =
   try Some (EvMap.find evk evtoid) with Not_found -> None
 
 let key id (_, idtoev) =
-  Idmap.find id idtoev
+  Id.Map.find id idtoev
 
 end
 
@@ -707,10 +707,10 @@ let extract_all_conv_pbs evd =
   extract_conv_pbs evd (fun _ -> true)
 
 let loc_of_conv_pb evd (pbty,env,t1,t2) =
-  match kind_of_term (fst (decompose_app t1)) with
+  match kind (fst (Term.decompose_app t1)) with
   | Evar (evk1,_) -> fst (evar_source evk1 evd)
   | _ ->
-  match kind_of_term (fst (decompose_app t2)) with
+  match kind (fst (Term.decompose_app t2)) with
   | Evar (evk2,_) -> fst (evar_source evk2 evd)
   | _             -> None
 
@@ -721,9 +721,9 @@ let loc_of_conv_pb evd (pbty,env,t1,t2) =
 
 let evars_of_term c =
   let rec evrec acc c =
-    match kind_of_term c with
+    match kind c with
     | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l)
-    | _ -> Term.fold_constr evrec acc c
+    | _ -> Constr.fold evrec acc c
   in
   evrec Evar.Set.empty c