diff options
| author | Matthieu Sozeau | 2015-11-27 20:34:51 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-11-27 21:01:59 +0100 |
| commit | 4a11dc25938f3f009e23f1e7c5fe01b2558928c3 (patch) | |
| tree | b9e68a7ff2082b25dd4ebc113d43ec9d0f691aa5 /library | |
| parent | a0e72610a71e086da392c8563c2eec2e35211afa (diff) | |
Univs: entirely disallow instantiation of polymorphic constants with
Prop levels.
As they are typed assuming all variables are >= Set now, and this was
breaking an invariant in typing. Only one instance in the standard
library was used in Hurkens, which can be avoided easily. This also
avoids displaying unnecessary >= Set constraints everywhere.
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 2 | ||||
| -rw-r--r-- | library/universes.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/library/declare.ml b/library/declare.ml index 5968fbf38b..994a6557ad 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -431,7 +431,7 @@ let cache_universes (p, l) = Univ.ContextSet.add_universe lev ctx)) (glob, Univ.ContextSet.empty) l in - Global.push_context_set false ctx; + Global.push_context_set p ctx; if p then Lib.add_section_context ctx; Universes.set_global_universe_names glob' diff --git a/library/universes.ml b/library/universes.ml index 1b6f7a9d57..a8e9478e13 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -820,7 +820,7 @@ let minimize_univ_variables ctx us algs left right cstrs = let cstrs' = List.fold_left (fun cstrs (d, r) -> if d == Univ.Le then enforce_leq inst (Universe.make r) cstrs - else + else try let lev = Option.get (Universe.level inst) in Constraint.add (lev, d, r) cstrs with Option.IsNone -> failwith "") |