From a9f0fd89cf3bb4b728eb451572a96f8599211380 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 30 Jan 2019 14:39:28 +0100
Subject: Separate variance and universe fields in inductives.

I think the usage looks cleaner this way.
---
 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 0cfc010c1a..a47fa78f4d 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -268,7 +268,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
         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 initunivs = UState.univ_entry ~poly initial_euctx in
           let ctx = constrain_variables universes in
           (* For vi2vo compilation proofs are computed now but we need to
              complement the univ constraints of the typ with the ones of
@@ -302,7 +302,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
     else
       fun t p ->
         (* Already checked the univ_decl for the type universes when starting the proof. *)
-        let univctx = Entries.Monomorphic_const_entry (UState.context_set universes) in
+        let univctx = UState.univ_entry ~poly:false universes in
         let t = nf t in
         Future.from_val (univctx, t),
         Future.chain p (fun (pt,eff) ->
-- 
cgit v1.2.3