diff options
| author | Pierre-Marie Pédrot | 2018-10-17 15:29:47 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-17 15:29:47 +0200 |
| commit | 15998894ff76b1fa9354085ea0bddae4f8f23ddf (patch) | |
| tree | 254cc3a53b6aa344f49a10cba32e14acf97d2905 /vernac/classes.ml | |
| parent | 063cf49f40511730c8c60c45332e92823ce4c78f (diff) | |
| parent | 6aa0aa37e19457a8c0c3ad36f7bbead058442344 (diff) | |
Merge PR #8694: Various cleanups of universe apis
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 |