diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-07 17:26:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-07 17:26:29 +0200 |
| commit | 2fbcbeece792c2f0e235160d66014150224fe7d7 (patch) | |
| tree | ff03867a1e665aca1bcb86b3cabc1cb1fc1e60cc /checker/environ.ml | |
| parent | 560b24f8eab0838fd6e01da8c4373f560020aadd (diff) | |
Removing 'open Univ' from checker.
Diffstat (limited to 'checker/environ.ml')
| -rw-r--r-- | checker/environ.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/checker/environ.ml b/checker/environ.ml index d23740ca7..a04e95cfc 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -1,7 +1,6 @@ open Errors open Util open Names -open Univ open Cic open Term open Declarations @@ -14,7 +13,7 @@ type globals = { env_modtypes : module_type_body MPmap.t} type stratification = { - env_universes : universes; + env_universes : Univ.universes; env_engagement : engagement option } @@ -77,12 +76,12 @@ let push_rec_types (lna,typarray,_) env = (* Universe constraints *) let add_constraints c env = - if c == Constraint.empty then + if c == Univ.Constraint.empty then env else let s = env.env_stratification in { env with env_stratification = - { s with env_universes = merge_constraints c s.env_universes } } + { s with env_universes = Univ.merge_constraints c s.env_universes } } let check_constraints cst env = Univ.check_constraints cst env.env_stratification.env_universes |