diff options
| author | Gaëtan Gilbert | 2018-12-04 16:22:18 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-12-17 14:49:13 +0100 |
| commit | a2ec08199d023b102df7806db8ed1e71c3ed27ce (patch) | |
| tree | 24d6607635a844f888c104309ee4f8d4c423a2e5 /kernel/univ.mli | |
| parent | 854d3e1b404fb3ee9087ffb07cbba7cc9196c1f9 (diff) | |
Make ugraph implementation abstract wrt universe specifics
This should give better visibility of universe specific operations vs
generic graph operations.
Diffstat (limited to 'kernel/univ.mli')
| -rw-r--r-- | kernel/univ.mli | 4 |
1 files changed, 2 insertions, 2 deletions
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 |