From c1cd47d5dff18f12af063d2c8defbd985c97dec6 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 14 Nov 2013 11:50:04 +0100
Subject: - Fix comparison of universes. - Shortcut for Set <= x checks,
 assuming that this is always true except when x (or rather its canonical
 representative) is Prop. Invariant to check. - Uncomment the profiling code
 and make it depend on a (statically known) boolean.

---
 proofs/refiner.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 663e24f9fc..da9e8c68d6 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -28,8 +28,11 @@ let refiner pr goal_sigma =
   { it = sgl; sigma = sigma'; }
 
 (* Profiling refiner *)
-(* let refiner_key = Profile.declare_profile "refiner" *)
-(* let refiner = Profile.profile2 refiner_key refiner *)
+let refiner = 
+  if Flags.profile then
+    let refiner_key = Profile.declare_profile "refiner" in
+      Profile.profile2 refiner_key refiner
+  else refiner
 
 (*********************)
 (*   Tacticals       *)
-- 
cgit v1.2.3