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.

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

(limited to 'kernel/vars.ml')

diff --git a/kernel/vars.ml b/kernel/vars.ml
index 3cff51ba6d..a9f4644abf 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -259,8 +259,11 @@ let subst_univs_constr subst c =
     let f = Univ.make_subst subst in
       subst_univs_fn_constr f c
 
-(* let subst_univs_constr_key = Profile.declare_profile "subst_univs_constr" *)
-(* let subst_univs_constr = Profile.profile2 subst_univs_constr_key subst_univs_constr *)
+let subst_univs_constr = 
+  if Flags.profile then
+    let subst_univs_constr_key = Profile.declare_profile "subst_univs_constr" in
+      Profile.profile2 subst_univs_constr_key subst_univs_constr
+  else subst_univs_constr
 
 let subst_univs_level_constr subst c =
   if Univ.is_empty_level_subst subst then c
-- 
cgit v1.2.3