diff options
Diffstat (limited to 'pretyping/evd.ml')
-rw-r--r-- | pretyping/evd.ml | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 166bab4b8..fd6af80b8 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -372,7 +372,12 @@ let process_universe_constraints univs vars alg local cstrs = else match Univ.Universe.level r with | None -> error ("Algebraic universe on the right") - | Some _ -> Univ.enforce_leq l r local + | Some rl when Univ.Level.is_small rl -> + (match Univ.Universe.level l with + | Some ll when Univ.LMap.mem ll !vars -> + Univ.enforce_eq l r local + | _ -> raise (Univ.UniverseInconsistency (Univ.Le, l, r, []))) + | _ -> Univ.enforce_leq l r local else if d == Univ.ULub then match varinfo l, varinfo r with | (Inr (l, true, _), Inr (r, _, _)) @@ -1107,6 +1112,11 @@ let set_leq_sort evd s1 s2 = | Prop c, Prop c' -> if c == Null && c' == Pos then evd else (raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, []))) + | Type u, Prop _ -> + (match is_sort_variable evd s1 with + | Some (_, false) -> + add_universe_constraints evd (Univ.UniverseConstraints.singleton (u1, Univ.UEq, u2)) + | _ -> raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, []))) | _, _ -> add_universe_constraints evd (Univ.UniverseConstraints.singleton (u1,Univ.ULe,u2)) |