diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-05 20:22:14 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-06 13:23:31 +0100 |
| commit | 5b8b02cd060097c3c980b0498257c30eda1ad207 (patch) | |
| tree | ff0e51230d3518bb2db523187644cd73d40aecf5 /vernac/classes.ml | |
| parent | 2c5e81e3bc6ec17d253aeedd1b2bf4ccd3b81933 (diff) | |
Fix #6323: stronger restrict universe context vs abstract.
In the test we do [let X : Type@{i} := Set in ...] with Set
abstracted. The constraint [Set < i] was lost in the abstract.
Universes of a monomorphic reference [c] are considered to appear in
the term [c].
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index cb1d2f7c7..3e47f881c 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -114,9 +114,10 @@ let instance_hook k info global imps ?hook cst = let declare_instance_constant k info global imps ?hook id decl poly evm term termtype = let kind = IsDefinition Instance in - let evm = - let levels = Univ.LSet.union (Univops.universes_of_constr termtype) - (Univops.universes_of_constr term) in + let evm = + let env = Global.env () in + let levels = Univ.LSet.union (Univops.universes_of_constr env termtype) + (Univops.universes_of_constr env term) in Evd.restrict_universe_context evm levels in let uctx = Evd.check_univ_decl ~poly evm decl in |