From 4cb7fe525a472928aee02d772458d28a2b71072a Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 7 Apr 2014 19:21:05 +0200 Subject: - Fix arity handling in retyping (de Bruijn bug!) - Enforce that no u <= Prop/Set can be added for u introduced by the user in Evd.process_constraints. (Needs to be enforced in the kernel as well, but that's the main entry point). - Fix a test-suite script and remove a regression comment, it's just as before now. --- pretyping/evd.ml | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) (limited to 'pretyping/evd.ml') 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)) -- cgit v1.2.3