From 84add29c036735ceacde73ea98a9a5a454a5e3a0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 6 Oct 2015 19:09:10 +0200
Subject: 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.
---
 pretyping/pretyping.ml     | 2 +-
 pretyping/reductionops.mli | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping')

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
-- 
cgit v1.2.3