From 05dff3bdaaf474e67b0878bc2dd0952427ce277e Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 22 Jun 2018 16:09:23 +0200 Subject: universes_of_constr don't include universes of monomorphic constants Apparently it was not useful. I don't remember what I was thinking when I added it. --- vernac/classes.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'vernac/classes.ml') 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 -- cgit v1.2.3