1 files changed, 23 insertions, 24 deletions

diff --git a/interp/declare.ml b/interp/declare.ml
index bd8f3db507..1a589897bd 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -14,8 +14,7 @@ open Util
 open Names
 open Libnames
 open Globnames
-open Nameops
-open Term
+open Constr
 open Declarations
 open Entries
 open Libobject
@@ -46,7 +45,7 @@ let cache_variable ((sp,_),o) =
   | Inr (id,(p,d,mk)) ->
   (* Constr raisonne sur les noms courts *)
   if variable_exists id then
-    alreadydeclared (pr_id id ++ str " already exists");
+    alreadydeclared (Id.print id ++ str " already exists");
 
   let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *)
     | SectionLocalAssum ((ty,ctx),poly,impl) ->
@@ -107,7 +106,7 @@ type constant_declaration = Safe_typing.private_constants constant_entry * logic
 (* section (if Remark or Fact) is needed to access a construction *)
 let load_constant i ((sp,kn), obj) =
   if Nametab.exists_cci sp then
-    alreadydeclared (pr_id (basename sp) ++ str " already exists");
+    alreadydeclared (Id.print (basename sp) ++ str " already exists");
   let con = Global.constant_of_delta_kn kn in
   Nametab.push (Nametab.Until i) sp (ConstRef con);
   add_constant_kind con obj.cst_kind
@@ -132,35 +131,35 @@ let exists_name id =
 
 let check_exists sp =
   let id = basename sp in
-  if exists_name id then alreadydeclared (pr_id id ++ str " already exists")
+  if exists_name id then alreadydeclared (Id.print id ++ str " already exists")
 
 let cache_constant ((sp,kn), obj) =
   let id = basename sp in
-  let _,dir,_ = repr_kn kn in
+  let _,dir,_ = KerName.repr kn in
   let kn' =
     match obj.cst_decl with
     | None ->
       if Global.exists_objlabel (Label.of_id (basename sp))
-      then constant_of_kn kn
+      then Constant.make1 kn
       else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".")
     | Some decl ->
       let () = check_exists sp in
       Global.add_constant dir id decl
   in
-  assert (eq_constant kn' (constant_of_kn kn));
-  Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
+  assert (Constant.equal kn' (Constant.make1 kn));
+  Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn));
   let cst = Global.lookup_constant kn' in
   add_section_constant (Declareops.constant_is_polymorphic cst) kn' cst.const_hyps;
   Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps;
-  add_constant_kind (constant_of_kn kn) obj.cst_kind
+  add_constant_kind (Constant.make1 kn) obj.cst_kind
 
 let discharged_hyps kn sechyps =
-  let (_,dir,_) = repr_kn kn in
+  let (_,dir,_) = KerName.repr kn in
   let args = Array.to_list (instance_from_variable_context sechyps) in
   List.rev_map (Libnames.make_path dir) args
 
 let discharge_constant ((sp, kn), obj) =
-  let con = constant_of_kn kn in
+  let con = Constant.make1 kn in
   let from = Global.lookup_constant con in
   let modlist = replacement_context () in
   let hyps,subst,uctx = section_segment_of_constant con in
@@ -311,9 +310,9 @@ let cache_inductive ((sp,kn),(dhyps,mie)) =
   let names = inductive_names sp kn mie in
   List.iter check_exists (List.map fst names);
   let id = basename sp in
-  let _,dir,_ = repr_kn kn in
+  let _,dir,_ = KerName.repr kn in
   let kn' = Global.add_mind dir id mie in
-  assert (eq_mind kn' (mind_of_kn kn));
+  assert (MutInd.equal kn' (MutInd.make1 kn));
   let mind = Global.lookup_mind kn' in
   add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps;
   Dischargedhypsmap.set_discharged_hyps sp dhyps;
@@ -384,7 +383,7 @@ let declare_projections mind =
 	let kn' = declare_constant id (ProjectionEntry entry,
 				       IsDefinition StructureComponent)
 	in
-	  assert(eq_constant kn kn')) kns; true,true
+	  assert(Constant.equal kn kn')) kns; true,true
     | Some None -> true,false
     | None -> false,false
 
@@ -407,11 +406,11 @@ let pr_rank i = pr_nth (i+1)
 let fixpoint_message indexes l =
   Flags.if_verbose Feedback.msg_info (match l with
   | [] -> anomaly (Pp.str "no recursive definition.")
-  | [id] -> pr_id id ++ str " is recursively defined" ++
+  | [id] -> Id.print id ++ str " is recursively defined" ++
       (match indexes with
 	 | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)"
 	 | _ -> mt ())
-  | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++
+  | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++
 		  spc () ++ str "are recursively defined" ++
 		  match indexes with
 		    | Some a -> spc () ++ str "(decreasing respectively on " ++
@@ -422,25 +421,25 @@ let fixpoint_message indexes l =
 let cofixpoint_message l =
   Flags.if_verbose Feedback.msg_info (match l with
   | [] -> anomaly (Pp.str "No corecursive definition.")
-  | [id] -> pr_id id ++ str " is corecursively defined"
-  | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++
+  | [id] -> Id.print id ++ str " is corecursively defined"
+  | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++
                     spc () ++ str "are corecursively defined"))
 
 let recursive_message isfix i l =
   (if isfix then fixpoint_message i else cofixpoint_message) l
 
 let definition_message id =
-  Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is defined")
+  Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined")
 
 let assumption_message id =
   (* Changing "assumed" to "declared", "assuming" referring more to
   the type of the object than to the name of the object (see
   discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *)
-  Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is declared")
+  Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared")
 
 (** Global universe names, in a different summary *)
 
-type universe_context_decl = polymorphic * Univ.universe_context_set
+type universe_context_decl = polymorphic * Univ.ContextSet.t
 
 let cache_universe_context (p, ctx) =
   Global.push_context_set p ctx;
@@ -458,7 +457,7 @@ let declare_universe_context poly ctx =
   Lib.add_anonymous_leaf (input_universe_context (poly, ctx))
 
 (* Discharged or not *)
-type universe_decl = polymorphic * (Id.t * Univ.universe_level) list
+type universe_decl = polymorphic * (Id.t * Univ.Level.t) list
 
 let cache_universes (p, l) =
   let glob = Global.global_universe_names () in
@@ -527,7 +526,7 @@ let do_constraint poly l =
        let names, _ = Global.global_universe_names () in
        try loc, Id.Map.find id names
        with Not_found ->
-         user_err ?loc ~hdr:"Constraint" (str "Undeclared universe " ++ pr_id id)
+         user_err ?loc ~hdr:"Constraint" (str "Undeclared universe " ++ Id.print id)
   in
   let in_section = Lib.sections_are_opened () in
   let () =