diff options
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 09e2b8df45..3cf5e9bfdf 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -9,6 +9,7 @@ (************************************************************************) (*i*) +module CVars = Vars open Names open EConstr open Nametab @@ -116,8 +117,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 levels = Univ.LSet.union (Univops.universes_of_constr termtype) - (Univops.universes_of_constr term) in + let levels = Univ.LSet.union (CVars.universes_of_constr termtype) + (CVars.universes_of_constr term) in Evd.restrict_universe_context sigma levels in let uctx = Evd.check_univ_decl ~poly sigma decl in |