[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.

6 files changed, 0 insertions, 41 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 285fea183b..5eb8a88698 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1182,13 +1182,6 @@ let evar_conv_x flags = evar_conv_x flags
 
 let evar_unify = conv_fun evar_conv_x
 
-(* Profiling *)
-let evar_conv_x =
-  if Flags.profile then
-    let evar_conv_xkey = CProfile.declare_profile "evar_conv_x" in
-      CProfile.profile6 evar_conv_xkey evar_conv_x
-  else evar_conv_x
-
 let evar_conv_hook_get, evar_conv_hook_set = Hook.make ~default:evar_conv_x ()
 
 let evar_conv_x flags = Hook.get evar_conv_hook_get flags
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 4083d3bc23..cb576a379a 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1038,13 +1038,6 @@ let nf_all env sigma =
 (********************************************************************)
 (*                         Conversion                               *)
 (********************************************************************)
-(*
-let fkey = CProfile.declare_profile "fhnf";;
-let fhnf info v = CProfile.profile2 fkey fhnf info v;;
-
-let fakey = CProfile.declare_profile "fhnf_apply";;
-let fhnf_apply info k h a = CProfile.profile4 fakey fhnf_apply info k h a;;
-*)
 
 let is_transparent e k =
   match Conv_oracle.get_strategy (Environ.oracle e) k with
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 064990f6bf..cdb86afa1a 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -249,17 +249,6 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty =
     | Construct (cstr, u) -> sigma, EConstr.of_constr (type_of_constructor env (cstr, EInstance.kind sigma u))
     | _ -> assert false
 
-(* Profiling *)
-(* let get_type_of polyprop lax env sigma c = *)
-(*   let f,_,_,_ = retype ~polyprop sigma in *)
-(*     if lax then f env c else anomaly_on_error (f env) c  *)
-
-(* let get_type_of_key = CProfile.declare_profile "get_type_of" *)
-(* let get_type_of = CProfile.profile5 get_type_of_key get_type_of *)
-
-(* let get_type_of ?(polyprop=true) ?(lax=false) env sigma c = *)
-(*   get_type_of polyprop lax env sigma c *)
-
 let get_type_of ?(polyprop=true) ?(lax=false) env sigma c =
   let f,_,_ = retype ~polyprop sigma in
     if lax then f env c else anomaly_on_error (f env) c
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 4e89018656..b59d4b5655 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1015,12 +1015,6 @@ let whd_simpl_orelse_delta_but_fix_old env sigma c =
   in app_stack (redrec (c, empty_stack))
 *)
 
-let whd_simpl_stack =
-  if Flags.profile then
-    let key = CProfile.declare_profile "whd_simpl_stack" in
-      CProfile.profile3 key whd_simpl_stack
-  else whd_simpl_stack
-
 (* Same as [whd_simpl] but also reduces constants that do not hide a
    reducible fix, but does this reduction of constants only until it
    immediately hides a non reducible fix or a cofix *)
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 51b228a640..dd1d27e4c5 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -242,10 +242,6 @@ let get_solve_all_instances, solve_all_instances_hook = Hook.make ()
 let solve_all_instances env evd filter unique split fail =
   Hook.get get_solve_all_instances env evd filter unique split fail
 
-(** Profiling resolution of typeclasses *)
-(* let solve_classeskey = CProfile.declare_profile "solve_typeclasses" *)
-(* let solve_problem = CProfile.profile5 solve_classeskey solve_problem *)
-
 let resolve_typeclasses ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ())
     ?(split=true) ?(fail=true) env evd =
   if not (has_typeclasses filter evd) then evd
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 18db75eed5..43d562f77d 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -2069,11 +2069,5 @@ let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 =
 let w_unify env evd cv_pb flags ty1 ty2 =
   w_unify env evd cv_pb ~flags:flags ty1 ty2
 
-let w_unify =
-  if Flags.profile then
-    let wunifkey = CProfile.declare_profile "w_unify" in
-      CProfile.profile6 wunifkey w_unify
-  else w_unify
-
 let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 =
   w_unify env evd cv_pb flags ty1 ty2