From ede4fa2f51bee0a425f68cd159178835a3af3ca6 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 4 Nov 2013 18:19:28 +0100
Subject: Restore reasonable performance by not allocating during universe
 checks, using a fast_compare_neq.

---
 pretyping/evd.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'pretyping/evd.ml')

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index ef93a827a6..21a0603c3f 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1021,6 +1021,9 @@ let is_sort_variable evd s =
     | None -> None)
   | _ -> None
 
+let is_flexible_level evd l = 
+  let uctx = evd.universes in
+    Univ.LMap.mem l uctx.uctx_univ_variables
 
 let is_eq_sort s1 s2 =
   if Sorts.equal s1 s2 then None
-- 
cgit v1.2.3