diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-04-07 19:21:05 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:59 +0200 |
| commit | 4cb7fe525a472928aee02d772458d28a2b71072a (patch) | |
| tree | 5934260488727e9c06871ce775376535c252f721 /pretyping/evd.ml | |
| parent | 2d6de8b102ea3cd05c5d193190faf787ccb84baa (diff) | |
- 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.
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)) |