Merge PR #8694: Various cleanups of universe apis

3 files changed, 15 insertions, 12 deletions

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 9ca91d62da..d57b931785 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -676,11 +676,15 @@ let build_case_scheme fa =
 (*   in  *)
   let funs =
     let (_,f,_) = fa in
-    try fst (Global.constr_of_global_in_context (Global.env ()) (Smartlocate.global_with_alias f))
+    try (let open GlobRef in
+         match Smartlocate.global_with_alias f with
+         | ConstRef c -> c
+         | IndRef _ | ConstructRef _ | VarRef _ -> assert false)
     with Not_found ->
       user_err ~hdr:"FunInd.build_case_scheme"
         (str "Cannot find " ++ Libnames.pr_qualid f) in
-  let first_fun,u = destConst  funs in
+  let sigma, (_,u) = Evd.fresh_constant_instance env sigma funs in
+  let first_fun = funs in
   let funs_mp = Constant.modpath first_fun in
   let first_fun_kn = try fst (find_Function_infos  first_fun).graph_ind with Not_found -> raise No_graph_found in
   let this_block_funs_indexes = get_funs_constant funs_mp first_fun in
@@ -688,7 +692,7 @@ let build_case_scheme fa =
   let prop_sort = InProp in
   let funs_indexes =
     let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
-    List.assoc_f Constant.equal (fst (destConst funs)) this_block_funs_indexes
+    List.assoc_f Constant.equal funs this_block_funs_indexes
   in
   let (ind, sf) =
 	 let ind = first_fun_kn,funs_indexes in
@@ -700,7 +704,7 @@ let build_case_scheme fa =
   let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in
   let sorts =
     (fun (_,_,x) ->
-       UnivGen.new_sort_in_family x
+       fst @@ UnivGen.fresh_sort_in_family x
     )
       fa
   in
@@ -718,7 +722,7 @@ let build_case_scheme fa =
       (Some princ_name)
       this_block_funs
       0
-      (prove_princ_for_struct (ref (Evd.from_env (Global.env ()))) false 0 [|fst (destConst funs)|])
+      (prove_princ_for_struct (ref (Evd.from_env (Global.env ()))) false 0 [|funs|])
   in
   ()
  
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 9fa333c629..ca3160f4c4 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -24,6 +24,7 @@ open Globnames
 open Nameops
 open CErrors
 open Util
+open UnivGen
 open Tacticals
 open Tacmach
 open Tactics
@@ -50,7 +51,7 @@ open Context.Rel.Declaration
 (* Ugly things which should not be here *)
 
 [@@@ocaml.warning "-3"]
-let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_global @@
+let coq_constant m s = EConstr.of_constr @@ constr_of_global @@
   Coqlib.find_reference "RecursiveDefinition" m s
 
 let arith_Nat = ["Coq"; "Arith";"PeanoNat";"Nat"]
@@ -62,7 +63,7 @@ let pr_leconstr_rd =
 
 let coq_init_constant s =
   EConstr.of_constr (
-    UnivGen.constr_of_global @@
+    constr_of_global @@
     Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s)
 [@@@ocaml.warning "+3"]
 
@@ -96,9 +97,6 @@ let type_of_const sigma t =
       Typeops.type_of_constant_in (Global.env()) (sp, u)
     |_ -> assert false
 
-let constr_of_global x = 
-  fst (Global.constr_of_global_in_context (Global.env ()) x)
-
 let constant sl s = constr_of_global (find_reference sl s)
 
 let const_of_ref = function
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 85e759d152..9585826109 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -8,6 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+module CVars = Vars
 open Ltac_plugin
 open Pp
 open Util
@@ -150,8 +151,8 @@ let ic_unsafe c = (*FIXME remove *)
 
 let decl_constant na univs c =
   let open Constr in
-  let vars = Univops.universes_of_constr c in
-  let univs = Univops.restrict_universe_context univs vars in
+  let vars = CVars.universes_of_constr c in
+  let univs = UState.restrict_universe_context univs vars in
   let univs = Monomorphic_const_entry univs in
   mkConst(declare_constant (Id.of_string na) 
             (DefinitionEntry (definition_entry ~opaque:true ~univs c),