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

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

(limited to 'checker/term.ml')

diff --git a/checker/term.ml b/checker/term.ml
index 0f8aa804f6..3372f9b6c3 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -11,7 +11,6 @@
 open Errors
 open Util
 open Names
-open Univ
 open Esubst
 
 open Cic
@@ -349,7 +348,7 @@ let compare_sorts s1 s2 = match s1, s2 with
   | Pos, Null -> false
   | Null, Pos -> false
   end
-| Type u1, Type u2 -> Universe.equal u1 u2
+| Type u1, Type u2 -> Univ.Universe.equal u1 u2
 | Prop _, Type _ -> false
 | Type _, Prop _ -> false
 
-- 
cgit v1.2.3