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.
---
 kernel/subtyping.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/subtyping.ml')

diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 58f3bcdf00..a00a462e1b 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -317,7 +317,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
 		  (* Check that the given definition does not add any constraint over
 		     the expected ones, so that it can be used in place of 
                      the original. *)
-		    if Univ.check_constraints ctx1 (Environ.universes env) then
+		    if UGraph.check_constraints ctx1 (Environ.universes env) then
 		      cstrs, env, inst2
 		    else error (IncompatibleConstraints ctx1)
 		with Univ.UniverseInconsistency incon -> 
-- 
cgit v1.2.3