diff options
| author | Pierre-Marie Pédrot | 2014-06-07 17:26:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-06-07 17:26:29 +0200 |
| commit | 2fbcbeece792c2f0e235160d66014150224fe7d7 (patch) | |
| tree | ff03867a1e665aca1bcb86b3cabc1cb1fc1e60cc /checker/typeops.ml | |
| parent | 560b24f8eab0838fd6e01da8c4373f560020aadd (diff) | |
Removing 'open Univ' from checker.
Diffstat (limited to 'checker/typeops.ml')
| -rw-r--r-- | checker/typeops.ml | 11 |
1 files changed, 5 insertions, 6 deletions
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 *) |