Checker: avoid using obsolete names from Names

9 files changed, 56 insertions, 52 deletions

diff --git a/checker/declarations.ml b/checker/declarations.ml
index 3ce312533..1fe02c8b6 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -73,32 +73,32 @@ let solve_delta_kn resolve kn =
       | Equiv kn1 -> kn1
       | Inline _ -> raise Not_found
   with Not_found ->
-    let mp,dir,l = repr_kn kn in
+    let mp,dir,l = KerName.repr kn in
     let new_mp = find_prefix resolve mp in
     if mp == new_mp then
       kn
     else
-      make_kn new_mp dir l
+      KerName.make new_mp dir l
 
 let gen_of_delta resolve x kn fix_can =
   let new_kn = solve_delta_kn resolve kn in
   if kn == new_kn then x else fix_can new_kn
 
 let constant_of_delta resolve con =
-  let kn = user_con con in
-  gen_of_delta resolve con kn (constant_of_kn_equiv kn)
+  let kn = Constant.user con in
+  gen_of_delta resolve con kn (Constant.make kn)
 
 let constant_of_delta2 resolve con =
-  let kn, kn' = canonical_con con, user_con con in
-  gen_of_delta resolve con kn (constant_of_kn_equiv kn')
+  let kn, kn' = Constant.canonical con, Constant.user con in
+  gen_of_delta resolve con kn (Constant.make kn')
 
 let mind_of_delta resolve mind =
-  let kn = user_mind mind in
-  gen_of_delta resolve mind kn (mind_of_kn_equiv kn)
+  let kn = MutInd.user mind in
+  gen_of_delta resolve mind kn (MutInd.make kn)
 
 let mind_of_delta2 resolve mind =
-  let kn, kn' = canonical_mind mind, user_mind mind in
-  gen_of_delta resolve mind kn (mind_of_kn_equiv kn')
+  let kn, kn' = MutInd.canonical mind, MutInd.user mind in
+  gen_of_delta resolve mind kn (MutInd.make kn')
 
 let find_inline_of_delta kn resolve =
   match Deltamap.find_kn kn resolve with
@@ -106,7 +106,7 @@ let find_inline_of_delta kn resolve =
     | _ -> raise Not_found
 
 let constant_of_delta_with_inline resolve con =
-  let kn1,kn2 = canonical_con con,user_con con in
+  let kn1,kn2 = Constant.canonical con, Constant.user con in
   try find_inline_of_delta kn2 resolve
   with Not_found ->
     try find_inline_of_delta kn1 resolve
@@ -137,17 +137,17 @@ let subst_mp sub mp =
   | Some (mp',_) -> mp'
 
 let subst_kn_delta sub kn =
- let mp,dir,l = repr_kn kn in
+ let mp,dir,l = KerName.repr kn in
   match subst_mp0 sub mp with
      Some (mp',resolve) ->
-      solve_delta_kn resolve (make_kn mp' dir l)
+      solve_delta_kn resolve (KerName.make mp' dir l)
    | None -> kn
 
 let subst_kn sub kn =
- let mp,dir,l = repr_kn kn in
+ let mp,dir,l = KerName.repr kn in
   match subst_mp0 sub mp with
      Some (mp',_) ->
-      make_kn mp' dir l
+      KerName.make mp' dir l
    | None -> kn
 
 exception No_subst
@@ -165,14 +165,14 @@ let gen_subst_mp f sub mp1 mp2 =
     | Some (mp1',_), Some (mp2',resolve2) -> Canonical, (f mp1' mp2'), resolve2
 
 let make_mind_equiv mpu mpc dir l =
-  let knu = make_kn mpu dir l in
-  if mpu == mpc then mind_of_kn knu
-  else mind_of_kn_equiv knu (make_kn mpc dir l)
+  let knu = KerName.make mpu dir l in
+  if mpu == mpc then MutInd.make1 knu
+  else MutInd.make knu (KerName.make mpc dir l)
 
 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
+  let kn1,kn2 = MutInd.user mind, MutInd.canonical mind in
+  let mp1,dir,l = KerName.repr kn1 in
+  let mp2,_,_ = KerName.repr kn2 in
   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
@@ -182,14 +182,14 @@ let subst_ind sub mind =
   with No_subst -> mind
 
 let make_con_equiv mpu mpc dir l =
-  let knu = make_kn mpu dir l in
-  if mpu == mpc then constant_of_kn knu
-  else constant_of_kn_equiv knu (make_kn mpc dir l)
+  let knu = KerName.make mpu dir l in
+  if mpu == mpc then Constant.make1 knu
+  else Constant.make knu (KerName.make mpc dir l)
 
 let subst_con0 sub con u =
-  let kn1,kn2 = user_con con,canonical_con con in
-  let mp1,dir,l = repr_kn kn1 in
-  let mp2,_,_ = repr_kn kn2 in
+  let kn1,kn2 = Constant.user con, Constant.canonical con in
+  let mp1,dir,l = KerName.repr kn1 in
+  let mp2,_,_ = KerName.repr kn2 in
   let rebuild_con mp1 mp2 = make_con_equiv mp1 mp2 dir l in
   let dup con = con, Const (con, u) in
   let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in
@@ -304,7 +304,9 @@ let subset_prefixed_by mp resolver =
     match hint with
       | Inline _ -> rslv
       | Equiv _ ->
-	if mp_in_mp mp (modpath kn) then Deltamap.add_kn kn hint rslv else rslv
+	if mp_in_mp mp (KerName.modpath kn)
+        then Deltamap.add_kn kn hint rslv
+        else rslv
   in
   Deltamap.fold mp_prefix kn_prefix resolver empty_delta_resolver
 
diff --git a/checker/environ.ml b/checker/environ.ml
index 7040fdda4..9352f71ef 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -112,7 +112,7 @@ let anomaly s = anomaly (Pp.str s)
 let add_constant kn cs env =
   if Cmap_env.mem kn env.env_globals.env_constants then
     Printf.ksprintf anomaly ("Constant %s is already defined")
-      (string_of_con kn);
+      (Constant.to_string kn);
   let new_constants =
     Cmap_env.add kn cs env.env_globals.env_constants in
   let new_globals =
@@ -172,12 +172,14 @@ let lookup_projection p env =
 let scrape_mind env kn=
   try
     KNmap.find kn env.env_globals.env_inductives_eq
-  with 
-      Not_found -> kn
+  with
+    Not_found -> kn
 
 let mind_equiv env (kn1,i1) (kn2,i2) =
   Int.equal i1 i2 &&
-  KerName.equal (scrape_mind env (user_mind kn1)) (scrape_mind env (user_mind kn2))
+  KerName.equal
+    (scrape_mind env (MutInd.user kn1))
+    (scrape_mind env (MutInd.user kn2))
 
 
 let lookup_mind kn env =
@@ -186,9 +188,9 @@ let lookup_mind kn env =
 let add_mind kn mib env =
   if Mindmap_env.mem kn env.env_globals.env_inductives then
     Printf.ksprintf anomaly ("Inductive %s is already defined")
-      (string_of_mind kn);
+      (MutInd.to_string kn);
   let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in
-  let kn1,kn2 =  user_mind kn,canonical_mind kn in
+  let kn1,kn2 =  MutInd.user kn, MutInd.canonical kn in
   let new_inds_eq = if KerName.equal kn1 kn2 then
     env.env_globals.env_inductives_eq
   else
@@ -205,7 +207,7 @@ let add_mind kn mib env =
 let add_modtype ln mtb env =
   if MPmap.mem ln env.env_globals.env_modtypes then
     Printf.ksprintf anomaly ("Module type %s is already defined")
-      (string_of_mp ln);
+      (ModPath.to_string ln);
   let new_modtypes = MPmap.add ln mtb env.env_globals.env_modtypes in
   let new_globals =
     { env.env_globals with
@@ -215,7 +217,7 @@ let add_modtype ln mtb env =
 let shallow_add_module mp mb env =
   if MPmap.mem mp env.env_globals.env_modules then
     Printf.ksprintf anomaly ("Module %s is already defined")
-      (string_of_mp mp);
+      (ModPath.to_string mp);
   let new_mods = MPmap.add mp mb env.env_globals.env_modules in
   let new_globals =
     { env.env_globals with
@@ -225,7 +227,7 @@ let shallow_add_module mp mb env =
 let shallow_remove_module mp env =
   if not (MPmap.mem mp env.env_globals.env_modules) then
     Printf.ksprintf anomaly ("Module %s is unknown")
-      (string_of_mp mp);
+      (ModPath.to_string mp);
   let new_mods = MPmap.remove mp env.env_globals.env_modules in
   let new_globals =
     { env.env_globals with
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 566df673c..fd5eaeb8b 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -32,11 +32,11 @@ let string_of_mp mp =
   if !Flags.debug then debug_string_of_mp mp else string_of_mp mp
 
 let prkn kn =
-  let (mp,_,l) = repr_kn kn in
+  let (mp,_,l) = KerName.repr kn in
   str(string_of_mp mp ^ "." ^ Label.to_string l)
 let prcon c =
-  let ck = canonical_con c in
-  let uk = user_con c in
+  let ck = Constant.canonical c in
+  let uk = Constant.user c in
   if KerName.equal ck uk then prkn uk else (prkn uk ++str"(="++prkn ck++str")")
 
 (* Same as noccur_between but may perform reductions.
@@ -528,7 +528,7 @@ let check_positivity env_ar mind params nrecp inds =
 (************************************************************************)
 
 let check_inductive env kn mib =
-  Flags.if_verbose ppnl (str "  checking ind: " ++ pr_mind kn); pp_flush ();
+  Flags.if_verbose ppnl (str "  checking ind: " ++ MutInd.print kn); pp_flush ();
   (* check mind_constraints: should be consistent with env *)
   let env = add_constraints (Univ.UContext.constraints mib.mind_universes) env in
   (* check mind_record : TODO ? check #constructor = 1 ? *)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 3ea5ed0d3..c07a35e35 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -18,7 +18,7 @@ let refresh_arity ar =
   let ctxt, hd = decompose_prod_assum ar in
   match hd with
       Sort (Type u) when not (Univ.is_univ_variable u) ->
-      let ul = Univ.Level.make empty_dirpath 1 in
+      let ul = Univ.Level.make DirPath.empty 1 in
       let u' = Univ.Universe.make ul in
       let cst = Univ.enforce_leq u u' Univ.empty_constraint in
       let ctx = Univ.ContextSet.make (Univ.LSet.singleton ul) cst in
@@ -70,7 +70,7 @@ let check_constant_declaration env kn cb =
 let lookup_module mp env =
   try Environ.lookup_module mp env
   with Not_found ->
-    failwith ("Unknown module: "^string_of_mp mp)
+    failwith ("Unknown module: "^ModPath.to_string mp)
 
 let mk_mtb mp sign delta =
   { mod_mp = mp;
diff --git a/checker/modops.ml b/checker/modops.ml
index 9f4375262..442f999bb 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -28,7 +28,7 @@ let error_not_match l _ =
 let error_no_such_label l = error ("No such label "^Label.to_string l)
 
 let error_no_such_label_sub l l1 =
-  let l1 = string_of_mp l1 in
+  let l1 = ModPath.to_string l1 in
   error ("The field "^
          Label.to_string l^" is missing in "^l1^".")
 
diff --git a/checker/print.ml b/checker/print.ml
index 9cd8fda5d..da8a6106f 100644
--- a/checker/print.ml
+++ b/checker/print.ml
@@ -122,7 +122,7 @@ let print_pure_constr csr =
 	| ("Coq"::_::l) -> l
 	| l             -> l
     in  List.iter (fun x -> print_string x; print_string ".") ls;*)
-      print_string (debug_string_of_mind sp)
+      print_string (MutInd.debug_to_string sp)
   and sp_con_display sp =
 (*    let dir,l = decode_kn sp in
     let ls =
@@ -131,7 +131,7 @@ let print_pure_constr csr =
 	| ("Coq"::_::l) -> l
 	| l             -> l
     in  List.iter (fun x -> print_string x; print_string ".") ls;*)
-      print_string (debug_string_of_con sp)
+      print_string (Constant.debug_to_string sp)
 
   in
     try
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index e41922573..46d21f6cc 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -103,7 +103,7 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
   in
   let eq_projection_body p1 p2 =
     let check eq f = if not (eq (f p1) (f p2)) then error () in
-    check eq_mind (fun x -> x.proj_ind);
+    check MutInd.equal (fun x -> x.proj_ind);
     check (==) (fun x -> x.proj_npars);
     check (==) (fun x -> x.proj_arg);
     check (eq_constr) (fun x -> x.proj_type);
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 64afd21b2..da9842a8d 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -92,7 +92,7 @@ let judge_of_constant_knowing_parameters env (kn,u as cst) paramstyp =
   let _cb =
     try lookup_constant kn env
     with Not_found ->
-      failwith ("Cannot find constant: "^string_of_con kn)
+      failwith ("Cannot find constant: "^Constant.to_string kn)
   in
   let ty, cu = type_of_constant_knowing_parameters env cst paramstyp in
   let () = check_constraints cu env in
@@ -178,7 +178,7 @@ let judge_of_inductive_knowing_parameters env (ind,u) (paramstyp:constr array) =
   let specif =
     try lookup_mind_specif env ind
     with Not_found ->
-      failwith ("Cannot find inductive: "^string_of_mind (fst ind))
+      failwith ("Cannot find inductive: "^MutInd.to_string (fst ind))
   in
   type_of_inductive_knowing_parameters env (specif,u) paramstyp
 
@@ -192,7 +192,7 @@ let judge_of_constructor env (c,u) =
   let specif =
     try lookup_mind_specif env ind
     with Not_found ->
-      failwith ("Cannot find inductive: "^string_of_mind (fst ind))
+      failwith ("Cannot find inductive: "^MutInd.to_string (fst ind))
   in
   type_of_constructor (c,u) specif
 
@@ -223,7 +223,7 @@ let judge_of_projection env p c ct =
     try find_rectype env ct
     with Not_found -> error_case_not_inductive env (c, ct)
   in
-    assert(eq_mind pb.proj_ind (fst ind));
+    assert(MutInd.equal pb.proj_ind (fst ind));
     let ty = subst_instance_constr u pb.proj_type in
       substl (c :: List.rev args) ty
 
diff --git a/kernel/names.mli b/kernel/names.mli
index 1dfdd8290..56f0f8c60 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -766,7 +766,7 @@ val mind_of_kn : KerName.t -> mutual_inductive
 (** @deprecated Same as [MutInd.make1] *)
 
 val mind_of_kn_equiv : KerName.t -> KerName.t -> mutual_inductive
-(** @deprecated Same as [MutInd.make2] *)
+(** @deprecated Same as [MutInd.make] *)
 
 val make_mind : ModPath.t -> DirPath.t -> Label.t -> mutual_inductive
 (** @deprecated Same as [MutInd.make3] *)