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.
---
 pretyping/tacred.ml | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'pretyping/tacred.ml')

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 *)
-- 
cgit v1.2.3