From 2fbcbeece792c2f0e235160d66014150224fe7d7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sat, 7 Jun 2014 17:26:29 +0200
Subject: Removing 'open Univ' from checker.

---
 checker/indtypes.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'checker/indtypes.ml')

diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index bfc20d7f8..14710c10b 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -9,7 +9,6 @@
 open Errors
 open Util
 open Names
-open Univ
 open Cic
 open Term
 open Inductive
@@ -183,7 +182,7 @@ let check_predicativity env s small level =
         (* let cst = *)
         (*   merge_constraints (enforce_leq u u' empty_constraint) *)
         (*     (universes env) in *)
-        if not (check_leq (universes env) level u) then
+        if not (Univ.check_leq (universes env) level u) then
           failwith "impredicative Type inductive type"
     | Prop Pos, Some ImpredicativeSet -> ()
     | Prop Pos, _ ->
-- 
cgit v1.2.3