From 5d3c0a0326af68e85f1f1cfc6bfa2214b0052de8 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 10 Mar 2020 01:06:34 -0400
Subject: [flags] [profile] Remove bit-rotten CProfile code.

As of today Coq has the `CProfile` infrastructure disabled by default,
untested, and not easily accessible.

It was decided that `CProfile` should remain not user-accessible, and
only available thus by manual editing of Coq code to switch the flag
and manually instrument functions.

We thus remove all bitrotten dead code.
---
 tactics/auto.ml    | 6 ------
 tactics/eauto.ml   | 3 ---
 tactics/tactics.ml | 6 ------
 3 files changed, 15 deletions(-)

(limited to 'tactics')

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 353e138599..0189e3ab04 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -500,12 +500,6 @@ let delta_auto debug mod_delta n lems dbnames =
     (search d n mod_delta db_list hints)
   end
 
-let delta_auto =
-  if Flags.profile then
-    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
 
 let new_auto ?(debug=Off) n = delta_auto debug true n
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 20c557b282..5df9fab236 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -359,9 +359,6 @@ let e_search_auto debug (in_depth,p) lems db_list =
     tclIDTAC gl
   end
 
-(* 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 =
   Hints.wrap_hint_warning (e_search_auto debug np lems db_list)
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index decf19588f..c24520b371 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1886,12 +1886,6 @@ let cut_and_apply c =
 (*               Exact tactics                                      *)
 (********************************************************************)
 
-(* let convert_leqkey = CProfile.declare_profile "convert_leq";; *)
-(* let convert_leq = CProfile.profile3 convert_leqkey convert_leq *)
-
-(* 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