Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.

6 files changed, 28 insertions, 28 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 2579ac045..7b921d35b 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -250,7 +250,7 @@ let cook_constant ~hcons env { from = cb; info } =
     cook_context = Some const_hyps;
   }
 
-(* let cook_constant_key = Profile.declare_profile "cook_constant" *)
-(* let cook_constant = Profile.profile2 cook_constant_key cook_constant *)
+(* let cook_constant_key = CProfile.declare_profile "cook_constant" *)
+(* let cook_constant = CProfile.profile2 cook_constant_key cook_constant *)
 
 let expmod_constr modlist c = expmod_constr (RefTable.create 13) modlist c
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 62aa9a2d7..2a629f00a 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -1098,8 +1098,8 @@ let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) =
     ()
 
 (*
-let cfkey = Profile.declare_profile "check_fix";;
-let check_fix env fix = Profile.profile3 cfkey check_fix env fix;;
+let cfkey = CProfile.declare_profile "check_fix";;
+let check_fix env fix = CProfile.profile3 cfkey check_fix env fix;;
 *)
 
 (************************************************************************)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index b0f4a1e5f..c07ac973b 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -833,8 +833,8 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 =
 let gen_conv cv_pb ?(l2r=false) ?(reds=full_transparent_state) env ?(evars=(fun _->None), universes env) =
   let evars, univs = evars in
   if Flags.profile then
-    let fconv_universes_key = Profile.declare_profile "trans_fconv_universes" in
-      Profile.profile8 fconv_universes_key gen_conv cv_pb l2r reds env evars univs
+    let fconv_universes_key = CProfile.declare_profile "trans_fconv_universes" in
+      CProfile.profile8 fconv_universes_key gen_conv cv_pb l2r reds env evars univs
   else gen_conv cv_pb l2r reds env evars univs
 
 let conv = gen_conv CONV
@@ -860,8 +860,8 @@ let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 =
 (* Profiling *)
 let infer_conv_universes = 
   if Flags.profile then 
-    let infer_conv_universes_key = Profile.declare_profile "infer_conv_universes" in
-      Profile.profile8 infer_conv_universes_key infer_conv_universes
+    let infer_conv_universes_key = CProfile.declare_profile "infer_conv_universes" in
+      CProfile.profile8 infer_conv_universes_key infer_conv_universes
   else infer_conv_universes
 
 let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_state)
@@ -895,13 +895,13 @@ let default_conv cv_pb ?(l2r=false) env t1 t2 =
 
 let default_conv_leq = default_conv CUMUL
 (*
-let convleqkey = Profile.declare_profile "Kernel_reduction.conv_leq";;
+let convleqkey = CProfile.declare_profile "Kernel_reduction.conv_leq";;
 let conv_leq env t1 t2 =
-  Profile.profile4 convleqkey conv_leq env t1 t2;;
+  CProfile.profile4 convleqkey conv_leq env t1 t2;;
 
-let convkey = Profile.declare_profile "Kernel_reduction.conv";;
+let convkey = CProfile.declare_profile "Kernel_reduction.conv";;
 let conv env t1 t2 =
-  Profile.profile4 convleqkey conv env t1 t2;;
+  CProfile.profile4 convleqkey conv env t1 t2;;
 *)
 
 (* Application with on-the-fly reduction *)
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 4ccef5c38..4a935f581 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -435,8 +435,8 @@ let infer env constr =
 
 let infer = 
   if Flags.profile then
-    let infer_key = Profile.declare_profile "Fast_infer" in
-      Profile.profile2 infer_key (fun b c -> infer b c)
+    let infer_key = CProfile.declare_profile "Fast_infer" in
+      CProfile.profile2 infer_key (fun b c -> infer b c)
   else (fun b c -> infer b c)
 
 let assumption_of_judgment env {uj_val=c; uj_type=t} =
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 00c0ea70d..f1e8d1031 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -890,24 +890,24 @@ let dump_universes output g =
 
 let merge_constraints = 
   if Flags.profile then 
-    let key = Profile.declare_profile "merge_constraints" in
-      Profile.profile2 key merge_constraints
+    let key = CProfile.declare_profile "merge_constraints" in
+      CProfile.profile2 key merge_constraints
   else merge_constraints
 let check_constraints =
   if Flags.profile then
-    let key = Profile.declare_profile "check_constraints" in
-      Profile.profile2 key check_constraints
+    let key = CProfile.declare_profile "check_constraints" in
+      CProfile.profile2 key check_constraints
   else check_constraints
 
 let check_eq = 
   if Flags.profile then
-    let check_eq_key = Profile.declare_profile "check_eq" in
-      Profile.profile3 check_eq_key check_eq
+    let check_eq_key = CProfile.declare_profile "check_eq" in
+      CProfile.profile3 check_eq_key check_eq
   else check_eq
 
 let check_leq = 
   if Flags.profile then 
-    let check_leq_key = Profile.declare_profile "check_leq" in
-      Profile.profile3 check_leq_key check_leq
+    let check_leq_key = CProfile.declare_profile "check_leq" in
+      CProfile.profile3 check_leq_key check_leq
   else check_leq
 
diff --git a/kernel/vars.ml b/kernel/vars.ml
index f52d734ef..eae917b5a 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -133,8 +133,8 @@ let substn_many lamv n c =
     substrec n c
 
 (*
-let substkey = Profile.declare_profile "substn_many";;
-let substn_many lamv n c = Profile.profile3 substkey substn_many lamv n c;;
+let substkey = CProfile.declare_profile "substn_many";;
+let substn_many lamv n c = CProfile.profile3 substkey substn_many lamv n c;;
 *)
 
 let make_subst = function
@@ -274,8 +274,8 @@ let subst_univs_constr subst c =
 
 let subst_univs_constr = 
   if Flags.profile then
-    let subst_univs_constr_key = Profile.declare_profile "subst_univs_constr" in
-      Profile.profile2 subst_univs_constr_key subst_univs_constr
+    let subst_univs_constr_key = CProfile.declare_profile "subst_univs_constr" in
+      CProfile.profile2 subst_univs_constr_key subst_univs_constr
   else subst_univs_constr
 
 let subst_univs_level_constr subst c =
@@ -347,8 +347,8 @@ let subst_instance_constr subst c =
     in
     aux c
 
-(* let substkey = Profile.declare_profile "subst_instance_constr";; *)
-(* let subst_instance_constr inst c = Profile.profile2 substkey subst_instance_constr inst c;; *)
+(* let substkey = CProfile.declare_profile "subst_instance_constr";; *)
+(* let subst_instance_constr inst c = CProfile.profile2 substkey subst_instance_constr inst c;; *)
 
 let subst_instance_context s ctx = 
   if Univ.Instance.is_empty s then ctx