diff options
| author | Matthieu Sozeau | 2014-04-07 19:21:05 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:59 +0200 |
| commit | 4cb7fe525a472928aee02d772458d28a2b71072a (patch) | |
| tree | 5934260488727e9c06871ce775376535c252f721 /library | |
| 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 'library')
| -rw-r--r-- | library/universes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/universes.ml b/library/universes.ml index 7d1908d1f5..f1c9c85a20 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -645,7 +645,7 @@ let universes_of_constr c = match kind_of_term c with | Const (_, u) | Ind (_, u) | Construct (_, u) -> LSet.union (Instance.levels u) s - | Sort u -> + | Sort u when not (Sorts.is_small u) -> let u = univ_of_sort u in LSet.union (Universe.levels u) s | _ -> fold_constr aux s c |