- 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.

3 files changed, 26 insertions, 13 deletions

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| *)
 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 21a0603c3f..52e37e611b 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -328,7 +328,7 @@ let diff_evar_universe_context ctx' ctx  =
 	uctx_universes = Univ.empty_universes }
 
 (* let diff_evar_universe_context_key = Profile.declare_profile "diff_evar_universe_context";; *)
-(* let diff_evar_universe_context =  *)
+(* let diff_evar_universe_context = *)
 (*   Profile.profile2 diff_evar_universe_context_key diff_evar_universe_context;; *)
 
 type 'a in_evar_universe_context = 'a * evar_universe_context
@@ -360,8 +360,9 @@ let process_universe_constraints univs postponed vars alg local cstrs =
 	in
 	  if d == Univ.ULe then
 	    if Univ.check_leq univs l r then
-	      (** Keep Prop <= var around if var might be instantiated by prop later. *)
-	      if Univ.is_type0m_univ l && not (Univ.is_small_univ r) then
+	      (** Keep Prop/Set <= var around if var might be instantiated by prop or set
+		  later. *)
+	      if Univ.is_small_univ l && not (Univ.is_small_univ r) then
 		match Univ.Universe.level l, Univ.Universe.level r with
 		| Some l, Some r -> Univ.Constraint.add (l,Univ.Le,r) local, postponed
 		| _, _ -> local, postponed
@@ -899,6 +900,9 @@ let merge orig ext =
       universes;
       metas = merge_metas orig.metas ext.metas }
 
+(* let merge_key = Profile.declare_profile "merge" *)
+(* let merge = Profile.profile2 merge_key merge *)
+
 (**********************************************************)
 (* Sort variables *)
 
@@ -1243,8 +1247,11 @@ let nf_constraints evd =
   let uctx' = normalize_evar_universe_context uctx' in
     {evd with universes = uctx'}
 
-(* let nfconstrkey = Profile.declare_profile "nf_constraints";; *)
-(* let nf_constraints = Profile.profile1 nfconstrkey nf_constraints;; *)
+let nf_constraints = 
+  if Flags.profile then
+    let nfconstrkey = Profile.declare_profile "nf_constraints" in
+      Profile.profile1 nfconstrkey nf_constraints
+  else nf_constraints
 
 let universes evd = evd.universes.uctx_universes
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index dbd83bb42a..3bb3aa9baf 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1370,12 +1370,15 @@ let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 =
       | _ -> w_typed_unify env evd cv_pb flags ty1 ty2
 
 (* Profiling *)
-(* let wunifkey = Profile.declare_profile "w_unify";; *)
 
-(* let w_unify env evd cv_pb flags ty1 ty2 = *)
-(*   w_unify env evd cv_pb ~flags:flags ty1 ty2 *)
+let w_unify env evd cv_pb flags ty1 ty2 =
+  w_unify env evd cv_pb ~flags:flags ty1 ty2
 
-(* let w_unify = Profile.profile6 wunifkey w_unify *)
+let w_unify = 
+  if Flags.profile then
+    let wunifkey = Profile.declare_profile "w_unify" in
+      Profile.profile6 wunifkey w_unify
+  else w_unify
 
-(* let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 = *)
-(*   w_unify env evd cv_pb flags ty1 ty2 *)
+let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 =
+  w_unify env evd cv_pb flags ty1 ty2