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
---
 proofs/proof_global.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index de151fb6e5..25cf789193 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -347,8 +347,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
           not (Safe_typing.empty_private_constants = eff))
         in
         let typ = if allow_deferred then t else nf t in
-        let used_univs_body = Univops.universes_of_constr body in
-        let used_univs_typ = Univops.universes_of_constr typ in
+        let used_univs_body = Vars.universes_of_constr body in
+        let used_univs_typ = Vars.universes_of_constr typ in
         if allow_deferred then
           let initunivs = UState.const_univ_entry ~poly initial_euctx in
           let ctx = constrain_variables universes in
-- 
cgit v1.2.3