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.
---
 plugins/ltac/rewrite.ml | 8 --------
 1 file changed, 8 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index c7bda43465..1640bff43b 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -373,11 +373,6 @@ end) = struct
 
 end
 
-(* let my_type_of env evars c = Typing.e_type_of env evars c *)
-(* let mytypeofkey = CProfile.declare_profile "my_type_of";; *)
-(* let my_type_of = CProfile.profile3 mytypeofkey my_type_of *)
-
-
 let type_app_poly env env evd f args =
   let evars, c = app_poly_nocheck env evd f args in
   let evd', t = Typing.type_of env (goalevars evars) c in
@@ -2066,9 +2061,6 @@ let get_hyp gl (c,l) clause l2r =
 
 let general_rewrite_flags = { under_lambdas = false; on_morphisms = true }
 
-(* let rewriteclaustac_key = CProfile.declare_profile "cl_rewrite_clause_tac";; *)
-(* let cl_rewrite_clause_tac = CProfile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *)
-
 (** Setoid rewriting when called with "rewrite" *)
 let general_s_rewrite cl l2r occs (c,l) ~new_goals =
   Proofview.Goal.enter begin fun gl ->
-- 
cgit v1.2.3