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/typeops.ml | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

(limited to 'checker/typeops.ml')

diff --git a/checker/typeops.ml b/checker/typeops.ml
index a0640a55f3..77fc4af739 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -9,7 +9,6 @@
 open Errors
 open Util
 open Names
-open Univ
 open Cic
 open Term
 open Reduction
@@ -53,11 +52,11 @@ let assumption_of_judgment env j =
 
 (* Prop and Set *)
 
-let judge_of_prop = Sort (Type type1_univ)
+let judge_of_prop = Sort (Type Univ.type1_univ)
 
 (* Type of Type(i). *)
 
-let judge_of_type u = Sort (Type (super u))
+let judge_of_type u = Sort (Type (Univ.super u))
 
 (*s Type of a de Bruijn index. *)
 
@@ -134,13 +133,13 @@ let sort_of_product env domsort rangsort =
           rangsort
         else
           (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
-          Type (sup u1 type0_univ)
+          Type (Univ.sup u1 Univ.type0_univ)
     (* Product rule (Prop,Type_i,Type_i) *)
-    | (Prop Pos,  Type u2)  -> Type (sup type0_univ u2)
+    | (Prop Pos,  Type u2)  -> Type (Univ.sup Univ.type0_univ u2)
     (* Product rule (Prop,Type_i,Type_i) *)
     | (Prop Null, Type _)  -> rangsort
     (* Product rule (Type_i,Type_i,Type_i) *)
-    | (Type u1, Type u2) -> Type (sup u1 u2)
+    | (Type u1, Type u2) -> Type (Univ.sup u1 u2)
 
 (* Type of a type cast *)
 
-- 
cgit v1.2.3