From a51dda2344679dc6d9145f3f34acad29721f6c75 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 28 Apr 2018 19:26:21 +0200
Subject: Split off Universes functions dealing with generating new universes.

---
 proofs/tacmach.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index c1d69dfc54..092bb5c276 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -75,7 +75,7 @@ let pf_ids_set_of_hyps gls =
 let pf_get_new_id id gls =
   next_ident_away id (pf_ids_set_of_hyps gls)
 
-let pf_global gls id = EConstr.of_constr (Universes.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id))
+let pf_global gls id = EConstr.of_constr (UnivGen.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id))
 
 let pf_reduction_of_red_expr gls re c =
   let (redfun, _) = reduction_of_red_expr (pf_env gls) re in
-- 
cgit v1.2.3


From 302adae094bbf76d8c951c557c85acb12a97aedc Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 28 Apr 2018 21:27:15 +0200
Subject: Split off Universes functions about substitutions and constraints

---
 proofs/proof_global.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 842003bc86..97cfccb8de 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -342,7 +342,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
      normalise them for the kernel. *)
   let subst_evar k =
     Proof.in_proof proof (fun m -> Evd.existential_opt_value0 m k) in
-  let nf = Universes.nf_evars_and_universes_opt_subst subst_evar
+  let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar
     (UState.subst universes) in
   let make_body =
     if poly || now then
-- 
cgit v1.2.3