diff options
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 382d18b09..26d105ecf 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -116,9 +116,8 @@ let instance_hook k info global imps ?hook cst = let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype = let kind = IsDefinition Instance in let sigma = - let env = Global.env () in - let levels = Univ.LSet.union (Univops.universes_of_constr env termtype) - (Univops.universes_of_constr env term) in + let levels = Univ.LSet.union (Univops.universes_of_constr termtype) + (Univops.universes_of_constr term) in Evd.restrict_universe_context sigma levels in let uctx = Evd.check_univ_decl ~poly sigma decl in |