From d0f89f8c59cda2e7e74fec693e511e910fbc0434 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 5 Dec 2017 12:34:36 +0100
Subject: [lib] Rename Profile to CProfile

New module introduced in OCaml 4.05 I think, can create problems when
linking with the OCaml toplevel for `Drop`.
---
 tactics/auto.ml    | 4 ++--
 tactics/eauto.ml   | 4 ++--
 tactics/tactics.ml | 8 ++++----
 3 files changed, 8 insertions(+), 8 deletions(-)

(limited to 'tactics')

diff --git a/tactics/auto.ml b/tactics/auto.ml
index fa8435d1ff..e7e21b5f4b 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -514,8 +514,8 @@ let delta_auto debug mod_delta n lems dbnames =
 
 let delta_auto = 
   if Flags.profile then
-    let key = Profile.declare_profile "delta_auto" in
-      Profile.profile5 key delta_auto
+    let key = CProfile.declare_profile "delta_auto" in
+      CProfile.profile5 key delta_auto
   else delta_auto
 
 let auto ?(debug=Off) n = delta_auto debug false n
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index f5c6ab8799..b5cfbe68b4 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -405,8 +405,8 @@ let e_search_auto debug (in_depth,p) lems db_list gl =
     pr_info_nop d;
     user_err Pp.(str "eauto: search failed")
 
-(* let e_search_auto_key = Profile.declare_profile "e_search_auto" *)
-(* let e_search_auto = Profile.profile5 e_search_auto_key e_search_auto *)
+(* let e_search_auto_key = CProfile.declare_profile "e_search_auto" *)
+(* let e_search_auto = CProfile.profile5 e_search_auto_key e_search_auto *)
 
 let eauto_with_bases ?(debug=Off) np lems db_list =
   tclTRY (e_search_auto debug np lems db_list)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e072bd95f6..cb2a77558e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1976,11 +1976,11 @@ let cut_and_apply c =
 (*               Exact tactics                                      *)
 (********************************************************************)
 
-(* let convert_leqkey = Profile.declare_profile "convert_leq";; *)
-(* let convert_leq = Profile.profile3 convert_leqkey convert_leq *)
+(* let convert_leqkey = CProfile.declare_profile "convert_leq";; *)
+(* let convert_leq = CProfile.profile3 convert_leqkey convert_leq *)
 
-(* let refine_no_checkkey = Profile.declare_profile "refine_no_check";; *)
-(* let refine_no_check = Profile.profile2 refine_no_checkkey refine_no_check *)
+(* let refine_no_checkkey = CProfile.declare_profile "refine_no_check";; *)
+(* let refine_no_check = CProfile.profile2 refine_no_checkkey refine_no_check *)
 
 let exact_no_check c =
   Refine.refine ~typecheck:false (fun h -> (h,c))
-- 
cgit v1.2.3