From 5bf063c15468bb81f0f48b583f600250cd829aee Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Oct 2018 13:37:46 +0200
Subject: UnivGen.constr_of_glob_univ -> Constr.mkRef

---
 vernac/comAssumption.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/comAssumption.ml')

diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 9497f2fb03..0ef5d56d4f 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -173,7 +173,7 @@ let do_assumptions kind nl l =
       let t = replace_vars subst t in
       let refs, status' = declare_assumptions idl is_coe kind (t,uctx) ubinders imps nl in
       let subst' = List.map2
-          (fun {CAst.v=id} (c,u) -> (id, UnivGen.constr_of_global_univ (c,u)))
+          (fun {CAst.v=id} (c,u) -> (id, Constr.mkRef (c,u)))
           idl refs
       in
       subst'@subst, status' && status, next_uctx uctx)
-- 
cgit v1.2.3


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/comAssumption.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/comAssumption.ml')

diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 0ef5d56d4f..e990f0cd15 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -162,7 +162,7 @@ let do_assumptions kind nl l =
   let nf_evar c = EConstr.to_constr sigma c in
   let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) ->
       let t = nf_evar t in
-      let uvars = Univ.LSet.union uvars (Univops.universes_of_constr t) in
+      let uvars = Univ.LSet.union uvars (Vars.universes_of_constr t) in
       uvars, (coe,t,imps))
       Univ.LSet.empty l
   in
-- 
cgit v1.2.3