diff options
Diffstat (limited to 'kernel/univ.ml')
| -rw-r--r-- | kernel/univ.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index d7c0cf13ec..8940c0337e 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -533,9 +533,9 @@ open Universe let universe_level = Universe.level -type constraint_type = Lt | Le | Eq +type constraint_type = AcyclicGraph.constraint_type = Lt | Le | Eq -type explanation = (constraint_type * universe) list +type explanation = (constraint_type * Level.t) list let constraint_type_ord c1 c2 = match c1, c2 with | Lt, Lt -> 0 @@ -1269,7 +1269,7 @@ let hcons_universe_context_set (v, c) = let hcons_univ x = Universe.hcons x -let explain_universe_inconsistency prl (o,u,v,p) = +let explain_universe_inconsistency prl (o,u,v,p : univ_inconsistency) = let pr_uni = Universe.pr_with prl in let pr_rel = function | Eq -> str"=" | Lt -> str"<" | Le -> str"<=" @@ -1281,9 +1281,9 @@ let explain_universe_inconsistency prl (o,u,v,p) = if p = [] then mt () else str " because" ++ spc() ++ pr_uni v ++ - prlist (fun (r,v) -> spc() ++ pr_rel r ++ str" " ++ pr_uni v) + prlist (fun (r,v) -> spc() ++ pr_rel r ++ str" " ++ prl v) p ++ - (if Universe.equal (snd (List.last p)) u then mt() else + (if Universe.equal (Universe.make (snd (List.last p))) u then mt() else (spc() ++ str "= " ++ pr_uni u)) in str "Cannot enforce" ++ spc() ++ pr_uni u ++ spc() ++ |