diff options
| author | Matthieu Sozeau | 2014-04-08 15:59:36 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:59 +0200 |
| commit | 4bfb3331804fd191a1d5fb92e99ae17b080f4f7b (patch) | |
| tree | e3c56f70fc23adc16fc365ee1fb60763e393a005 /pretyping | |
| parent | 4d779fe8ff9c2b81eddb671dc0e60d3743357ce5 (diff) | |
Fix set_leq_sort refusing max(u,Set) <= Set when u is flexible.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evd.ml | 14 |
1 files changed, 5 insertions, 9 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index fd6af80b89..652bed5a36 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -373,10 +373,11 @@ let process_universe_constraints univs vars alg local cstrs = match Univ.Universe.level r with | None -> error ("Algebraic universe on the right") | 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, []))) + (if Univ.LSet.for_all (fun l -> + Univ.Level.is_small l || Univ.LMap.mem l !vars) + (Univ.Universe.levels l) then + Univ.enforce_leq l r local + else 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 @@ -1112,11 +1113,6 @@ 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)) |