aboutsummaryrefslogtreecommitdiff
path: root/lib/flags.mli
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-03-10 01:06:34 -0400
committerEmilio Jesus Gallego Arias2021-03-30 15:37:00 +0200
commit5d3c0a0326af68e85f1f1cfc6bfa2214b0052de8 (patch)
tree4306352ac9163de2562ed3600ac468d26284d05a /lib/flags.mli
parent6effcc263beded0d530d724fab8edae86815adf8 (diff)
[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.
Diffstat (limited to 'lib/flags.mli')
-rw-r--r--lib/flags.mli2
1 files changed, 0 insertions, 2 deletions
diff --git a/lib/flags.mli b/lib/flags.mli
index e10e2c8cb8..2f59a0cc18 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -44,8 +44,6 @@ val xml_debug : bool ref
val in_debugger : bool ref
val in_toplevel : bool ref
-val profile : bool
-
(* development flag to detect race conditions, it should go away. *)
val we_are_parsing : bool ref