From a2ec08199d023b102df7806db8ed1e71c3ed27ce Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 4 Dec 2018 16:22:18 +0100
Subject: Make ugraph implementation abstract wrt universe specifics

This should give better visibility of universe specific operations vs
generic graph operations.
---
 kernel/univ.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/univ.mli')

diff --git a/kernel/univ.mli b/kernel/univ.mli
index d7097be570..b83251e983 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -166,7 +166,7 @@ val univ_level_rem : Level.t -> Universe.t -> Universe.t -> Universe.t
 
 (** {6 Constraints. } *)
 
-type constraint_type = Lt | Le | Eq
+type constraint_type = AcyclicGraph.constraint_type = Lt | Le | Eq
 type univ_constraint = Level.t * constraint_type * Level.t
 
 module Constraint : sig
@@ -203,7 +203,7 @@ val enforce_leq_level : Level.t constraint_function
   system stores the graph and may result from combination of several
   Constraint.t...
 *)
-type explanation = (constraint_type * Universe.t) list
+type explanation = (constraint_type * Level.t) list
 type univ_inconsistency = constraint_type * Universe.t * Universe.t * explanation Lazy.t option
 
 exception UniverseInconsistency of univ_inconsistency
-- 
cgit v1.2.3