diff options
| author | Pierre-Marie Pédrot | 2015-10-06 19:09:10 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-06 20:09:06 +0200 |
| commit | 84add29c036735ceacde73ea98a9a5a454a5e3a0 (patch) | |
| tree | baee8c0b023277d43366996685503c9d1f855413 /pretyping | |
| parent | c4db6fc1086d984fd983ff9a6797ad108d220b98 (diff) | |
Splitting kernel universe code in two modules.
1. The Univ module now only cares about definitions about universes.
2. The UGraph module contains the algorithm responsible for aciclicity.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 2 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 2efd8fe413..6373e60791 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -111,7 +111,7 @@ let interp_universe_level_name evd s = let level = Univ.Level.make dp num in let evd = try Evd.add_global_univ evd level - with Univ.AlreadyDeclared -> evd + with UGraph.AlreadyDeclared -> evd in evd, level else try diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 1df2a73b2e..5e1c467c82 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -251,7 +251,7 @@ type conversion_test = constraints -> constraints val pb_is_equal : conv_pb -> bool val pb_equal : conv_pb -> conv_pb -val sort_cmp : env -> conv_pb -> sorts -> sorts -> universes -> unit +val sort_cmp : env -> conv_pb -> sorts -> sorts -> UGraph.t -> unit val is_conv : env -> evar_map -> constr -> constr -> bool val is_conv_leq : env -> evar_map -> constr -> constr -> bool |