From 44ecd58e9ab5fb0f2c45e9eec76440f84995825c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Oct 2018 14:20:51 +0200
Subject: {Univops -> Vars}.universes_of_constr

It's basically an occur check so it makes sense to put it in vars
---
 vernac/classes.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'vernac/classes.ml')

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
-- 
cgit v1.2.3