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/inductive.ml | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'kernel/inductive.ml')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index eb18d4b90e..6cb61174d3 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -1334,11 +1334,6 @@ let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) =
   else
     ()
 
-(*
-let cfkey = CProfile.declare_profile "check_fix";;
-let check_fix env fix = CProfile.profile3 cfkey check_fix env fix;;
-*)
-
 (************************************************************************)
 (* Co-fixpoints. *)
 
-- 
cgit v1.2.3