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.

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

(limited to 'pretyping/evarconv.ml')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 594481af30..098f5ada5e 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -695,8 +695,11 @@ and eta_constructor ts env evd ((ind, i), u) l1 csts1 (c, csts2) =
     | _ -> UnifFailure (evd,NotSameHead)
 
 (* Profiling *)
-(* let evar_conv_xkey = Profile.declare_profile "evar_conv_x";; *)
-(* let evar_conv_x = Profile.profile6 evar_conv_xkey evar_conv_x *)
+let evar_conv_x =
+  if Flags.profile then
+    let evar_conv_xkey = Profile.declare_profile "evar_conv_x" in
+      Profile.profile6 evar_conv_xkey evar_conv_x
+  else evar_conv_x
 
 (* We assume here |l1| <= |l2| *)
 
-- 
cgit v1.2.3