From 4cb7fe525a472928aee02d772458d28a2b71072a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 7 Apr 2014 19:21:05 +0200
Subject: - Fix arity handling in retyping (de Bruijn bug!) - Enforce that no u
 <= Prop/Set can be added for u introduced by the user in
 Evd.process_constraints. (Needs to be enforced in the kernel as well, but
 that's the main entry point). - Fix a test-suite script and remove a
 regression comment, it's just as before now.

---
 library/universes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/universes.ml b/library/universes.ml
index 7d1908d1f5..f1c9c85a20 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -645,7 +645,7 @@ let universes_of_constr c =
     match kind_of_term c with
     | Const (_, u) | Ind (_, u) | Construct (_, u) ->
       LSet.union (Instance.levels u) s
-    | Sort u -> 
+    | Sort u when not (Sorts.is_small u) -> 
       let u = univ_of_sort u in
 	LSet.union (Universe.levels u) s
     | _ -> fold_constr aux s c
-- 
cgit v1.2.3