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

(limited to 'kernel/typeops.ml')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 1b1aa84e6b..3a946fc03a 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -644,12 +644,6 @@ let infer env constr =
   let constr, t = execute env constr in
   make_judge constr t
 
-let infer =
-  if Flags.profile then
-    let infer_key = CProfile.declare_profile "Fast_infer" in
-      CProfile.profile2 infer_key (fun b c -> infer b c)
-  else (fun b c -> infer b c)
-
 let assumption_of_judgment env {uj_val=c; uj_type=t} =
   infer_assumption env c t
 
-- 
cgit v1.2.3