diff options
| author | Pierre-Marie Pédrot | 2018-12-19 16:28:50 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-12-19 16:28:50 +0100 |
| commit | c687f514b9d86c2873ff5a519cd0f3b9694cf6e8 (patch) | |
| tree | 4fefb3772de7000347f0884ba29358438d7b8032 /kernel/univ.mli | |
| parent | c3e9f5f8804c3b1da323cb0a7ba7d1e46ccf0849 (diff) | |
| parent | 1199cbc1a45e378e41f4b159c4c62db598173716 (diff) | |
Merge PR #9159: Make ugraph implementation abstract wrt universe specifics
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 |