diff options
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 |