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.
---
 dev/printers.mllib  | 1 +
 dev/top_printers.ml | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 07b48ed573..f19edf1c80 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -55,6 +55,7 @@ Monad
 
 Names
 Univ
+UGraph
 Esubst
 Uint31
 Sorts
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 0900bb0962..1d3d711ac7 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -221,7 +221,7 @@ let ppuniverseconstraints c = pp (Universes.Constraints.pr c)
 let ppuniverse_context_future c = 
   let ctx = Future.force c in
     ppuniverse_context ctx
-let ppuniverses u = pp (Univ.pr_universes Level.pr u)
+let ppuniverses u = pp (UGraph.pr_universes Level.pr u)
 let ppnamedcontextval e =
   pp (pr_named_context (Global.env ()) Evd.empty (named_context_of_val e))
 
-- 
cgit v1.2.3