[universes] deprecate constr_of_global

In favor of a constr_of_monomorphic_global function. When people
move to the new Coqlib interface they will also see this deprecation
message encouraging them to think about the best move.

This commit changes a few references to constr_of_global and replaces
them with a constr_of_monomorphic_global which makes it apparent that
this is not the function to call to globalize polymorphic references.

The remaining parts using constr_of_monomorphic_global are easily
identifiable using this: omega, btauto, ring, funind and auto_ind_decl
mainly (this fixes firstorder). What this means is that the symbols
registered for these tactics have to be monomorphic for now.

4 files changed, 14 insertions, 14 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 98d68d3db7..ad1114b733 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -414,9 +414,9 @@ let rewrite_until_var arg_num eq_ids : tactic =
 
 let rec_pte_id = Id.of_string "Hrec"
 let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
-  let coq_False = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type") in
-  let coq_True = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.type") in
-  let coq_I = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.I") in
+  let coq_False = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type") in
+  let coq_True = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.type") in
+  let coq_I = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.I") in
   let rec scan_type  context type_of_hyp : tactic =
     if isLetIn sigma type_of_hyp then
       let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in
@@ -1605,7 +1605,7 @@ let prove_principle_for_gen
     match !tcc_lemma_ref with
      | Undefined -> user_err Pp.(str "No tcc proof !!")
      | Value lemma -> EConstr.of_constr lemma
-     | Not_needed -> EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.I")
+     | Not_needed -> EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.I")
   in
 (*   let rec list_diff del_list check_list = *)
 (*     match del_list with *)
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 03a64988e4..a385a61ae0 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -116,7 +116,7 @@ let def_of_const t =
 
 [@@@ocaml.warning "-3"]
 let coq_constant s =
-  UnivGen.constr_of_global @@
+  UnivGen.constr_of_monomorphic_global @@
   Coqlib.gen_reference_in_modules "RecursiveDefinition"
     Coqlib.init_modules s;;
 
@@ -441,7 +441,7 @@ let jmeq () =
   try
     Coqlib.check_required_library Coqlib.jmeq_module_name;
     EConstr.of_constr @@
-    UnivGen.constr_of_global @@
+    UnivGen.constr_of_monomorphic_global @@
       Coqlib.lib_ref "core.JMeq.type"
   with e when CErrors.noncritical e -> raise (ToShow e)
 
@@ -449,7 +449,7 @@ let jmeq_refl () =
   try
     Coqlib.check_required_library Coqlib.jmeq_module_name;
     EConstr.of_constr @@
-    UnivGen.constr_of_global @@
+    UnivGen.constr_of_monomorphic_global @@
       Coqlib.lib_ref "core.JMeq.refl"
   with e when CErrors.noncritical e -> raise (ToShow e)
 
@@ -463,7 +463,7 @@ let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc")
 let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv")
 
 [@@@ocaml.warning "-3"]
-let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_global @@
+let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@
     Coqlib.find_reference "IndFun" ["Coq"; "Arith";"Wf_nat"] "well_founded_ltof"
 [@@@ocaml.warning "+3"]
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index b8973a18dc..b0842c3721 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -81,7 +81,7 @@ let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
 
 let make_eq () =
   try
-    EConstr.of_constr (UnivGen.constr_of_global (Coqlib.lib_ref "core.eq.type"))
+    EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.eq.type"))
   with _ -> assert false
 
 (* [generate_type g_to_f f graph i] build the completeness (resp. correctness) lemma type if [g_to_f = true]
@@ -511,7 +511,7 @@ and intros_with_rewrite_aux : Tacmach.tactic =
 			    intros_with_rewrite
 			  ] g
 			end
-                  | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type")) ->
+                  | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type")) ->
 		      Proofview.V82.of_tactic tauto g
 		  | Case(_,_,v,_) ->
 		      tclTHENLIST[
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index ca3160f4c4..f9df3aed45 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -51,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 @@ constr_of_global @@
+let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@
   Coqlib.find_reference "RecursiveDefinition" m s
 
 let arith_Nat = ["Coq"; "Arith";"PeanoNat";"Nat"]
@@ -63,7 +63,7 @@ let pr_leconstr_rd =
 
 let coq_init_constant s =
   EConstr.of_constr (
-    constr_of_global @@
+    UnivGen.constr_of_monomorphic_global @@
     Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s)
 [@@@ocaml.warning "+3"]
 
@@ -97,7 +97,7 @@ let type_of_const sigma t =
       Typeops.type_of_constant_in (Global.env()) (sp, u)
     |_ -> assert false
 
-let constant sl s = constr_of_global (find_reference sl s)
+let constant sl s = UnivGen.constr_of_monomorphic_global (find_reference sl s)
 
 let const_of_ref = function
     ConstRef kn -> kn
@@ -1241,7 +1241,7 @@ let get_current_subgoals_types () =
 
 exception EmptySubgoals
 let build_and_l sigma l =
-  let and_constr =  UnivGen.constr_of_global @@ Coqlib.lib_ref "core.and.type" in
+  let and_constr =  UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.and.type" in
   let conj_constr = Coqlib.build_coq_conj () in
   let mk_and p1 p2 =
     mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in