[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.

17 files changed, 60 insertions, 55 deletions

diff --git a/engine/univGen.ml b/engine/univGen.ml
index 23ab30eb75..130aa06f53 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -77,17 +77,14 @@ let fresh_global_instance ?loc ?names env gr =
   let u, ctx = fresh_global_instance ?loc ?names env gr in
   mkRef (gr, u), ctx
 
-let constr_of_global gr =
-  let c, ctx = fresh_global_instance (Global.env ()) gr in
-    if not (Univ.ContextSet.is_empty ctx) then
-      if Univ.LSet.is_empty (Univ.ContextSet.levels ctx) then
-        (* Should be an error as we might forget constraints, allow for now
-           to make firstorder work with "using" clauses *)
-        c
-      else CErrors.user_err ~hdr:"constr_of_global"
-          Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++
-              str " would forget universes.")
-    else c
+let constr_of_monomorphic_global gr =
+  if not (Global.is_polymorphic gr) then
+    fst (fresh_global_instance (Global.env ()) gr)
+  else CErrors.user_err ~hdr:"constr_of_global"
+      Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++
+          str " would forget universes.")
+
+let constr_of_global gr = constr_of_monomorphic_global gr
 
 let constr_of_global_univ = mkRef
 
diff --git a/engine/univGen.mli b/engine/univGen.mli
index c2e9d0c696..42756701dc 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -74,11 +74,16 @@ val extend_context : 'a in_universe_context_set -> ContextSet.t ->
 [@@ocaml.deprecated "Use [Univ.extend_in_context_set]"]
 
 (** Create a fresh global in the global environment, without side effects.
-    BEWARE: this raises an ANOMALY on polymorphic constants/inductives:
+    BEWARE: this raises an error on polymorphic constants/inductives:
     the constraints should be properly added to an evd.
     See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for
-    the proper way to get a fresh copy of a global reference. *)
+    the proper way to get a fresh copy of a polymorphic global reference. *)
+val constr_of_monomorphic_global : GlobRef.t -> constr
+
 val constr_of_global : GlobRef.t -> constr
+[@@ocaml.deprecated "constr_of_global will crash on polymorphic constants,\
+                     use [constr_of_monomorphic_global] if the reference is guaranteed to\
+                     be monomorphic, [Evarutil.new_global] or [Tacmach.New.pf_constr_of_global] otherwise"]
 
 (** Returns the type of the global reference, by creating a fresh instance of polymorphic
     references and computing their instantiated universe context. (side-effect on the
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index b9ad1ff6d8..07f50f6cd5 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -10,7 +10,7 @@
 
 open Constr
 
-let bt_lib_constr n = lazy (UnivGen.constr_of_global @@ Coqlib.lib_ref n)
+let bt_lib_constr n = lazy (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref n)
 
 let decomp_term sigma (c : Constr.t) =
   Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast sigma (EConstr.of_constr c)))
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 8fa676de44..b0c4785d7a 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -233,12 +233,11 @@ let ll_forall_tac prod backtrack id continue seq=
 
 (* special for compatibility with old Intuition *)
 
-let constant str = UnivGen.constr_of_global
-  @@ Coqlib.lib_ref str
+let constant str = Coqlib.lib_ref str
 
 let defined_connectives = lazy
-  [AllOccurrences, EvalConstRef (fst (Constr.destConst (constant "core.not.type")));
-   AllOccurrences, EvalConstRef (fst (Constr.destConst (constant "core.iff.type")))]
+  [AllOccurrences, EvalConstRef (destConstRef (constant "core.not.type"));
+   AllOccurrences, EvalConstRef (destConstRef (constant "core.iff.type"))]
 
 let normalize_evaluables=
   Proofview.Goal.enter begin fun gl ->
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
diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml
index 11d0a4a44d..ef60a23e80 100644
--- a/plugins/nsatz/nsatz.ml
+++ b/plugins/nsatz/nsatz.ml
@@ -135,7 +135,7 @@ let mul = function
   | (Const n,q) when eq_num n num_1 -> q
   | (p,q) -> Mul(p,q)
 
-let gen_constant n = lazy (UnivGen.constr_of_global (Coqlib.lib_ref n))
+let gen_constant n = lazy (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n))
 
 let tpexpr  = gen_constant "plugins.setoid_ring.pexpr"
 let ttconst = gen_constant "plugins.setoid_ring.const"
@@ -540,7 +540,7 @@ let nsatz lpol =
 
 let return_term t =
   let a =
-    mkApp (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.eq.refl",[|tllp ();t|]) in
+    mkApp (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.eq.refl",[|tllp ();t|]) in
   let a = EConstr.of_constr a in
   generalize [a]
 
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 09bd4cd352..d8adb17710 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -186,7 +186,8 @@ let reset_all () =
  To use the constant Zplus, one must type "Lazy.force coq_Zplus"
  This is the right way to access to Coq constants in tactics ML code *)
 
-let gen_constant k = lazy (k |> Coqlib.lib_ref |> UnivGen.constr_of_global |> EConstr.of_constr)
+let gen_constant k = lazy (k |> Coqlib.lib_ref |> UnivGen.constr_of_monomorphic_global
+                           |> EConstr.of_constr)
 
 
 (* Zarith *)
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 79418da27c..840a05e02b 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -26,11 +26,11 @@ let step_count = ref 0
 
 let node_count = ref 0
 
-let li_False = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type"))
-let li_and   = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.and.type"))
-let li_or    = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.or.type"))
+let li_False = lazy (destInd (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type"))
+let li_and   = lazy (destInd (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.and.type"))
+let li_or    = lazy (destInd (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.or.type"))
 
-let gen_constant n = lazy (UnivGen.constr_of_global (Coqlib.lib_ref n))
+let gen_constant n = lazy (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n))
 
 let l_xI = gen_constant "num.pos.xI"
 let l_xO = gen_constant "num.pos.xO"
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 9585826109..8dbef47fe1 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -206,7 +206,7 @@ let exec_tactic env evd n f args =
   let nf c = constr_of evd c in
   Array.map nf !tactic_res, Evd.universe_context_set evd
 
-let gen_constant n = lazy (EConstr.of_constr (UnivGen.constr_of_global (Coqlib.lib_ref n)))
+let gen_constant n = lazy (EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n)))
 let gen_reference n = lazy (Coqlib.lib_ref n)
 
 let coq_mk_Setoid = gen_constant "plugins.setoid_ring.Build_Setoid_Theory"
@@ -251,7 +251,7 @@ let plugin_modules =
     ]
 
 let my_constant c =
-  lazy (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c))
+  lazy (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c))
     [@@ocaml.warning "-3"]
 let my_reference c =
   lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c)
@@ -901,7 +901,7 @@ let ftheory_to_obj : field_info -> obj =
 let field_equality evd r inv req =
   match EConstr.kind !evd req with
     | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) ->
-        let c = UnivGen.constr_of_global Coqlib.(lib_ref "core.eq.congr") in
+        let c = UnivGen.constr_of_monomorphic_global Coqlib.(lib_ref "core.eq.congr") in
         let c = EConstr.of_constr c in
         mkApp(c,[|r;r;inv|])
     | _ ->
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 1492cfb4e4..6746eff223 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1220,7 +1220,7 @@ let genclrtac cl cs clr =
       (fun type_err gl ->
          tclTHEN
            (tclTHEN (Proofview.V82.of_tactic (Tactics.elim_type (EConstr.of_constr
-             (UnivGen.constr_of_global @@ Coqlib.(lib_ref "core.False.type"))))) (old_cleartac clr))
+             (UnivGen.constr_of_monomorphic_global @@ Coqlib.(lib_ref "core.False.type"))))) (old_cleartac clr))
            (fun gl -> raise type_err)
            gl))
     (old_cleartac clr)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 5d1faf1465..388bf8efb5 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -68,7 +68,10 @@ 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 (UnivGen.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id))
+let pf_global gls id =
+  let env = pf_env gls in
+  let sigma = project gls in
+  Evd.fresh_global env sigma (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
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 3432ad4afa..f302960870 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -34,7 +34,7 @@ val pf_hyps_types         : goal sigma -> (Id.t * types) list
 val pf_nth_hyp_id         : goal sigma -> int -> Id.t
 val pf_last_hyp           : goal sigma -> named_declaration
 val pf_ids_of_hyps        : goal sigma -> Id.t list
-val pf_global             : goal sigma -> Id.t -> constr
+val pf_global             : goal sigma -> Id.t -> evar_map * constr
 val pf_unsafe_type_of            : goal sigma -> constr -> types
 val pf_type_of            : goal sigma -> constr -> evar_map * types
 val pf_hnf_type_of        : goal sigma -> constr -> types
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 148d4437fa..9f71def8fc 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -63,20 +63,20 @@ exception ConstructorWithNonParametricInductiveType of inductive
 exception DecidabilityIndicesNotSupported
 
 (* Some pre declaration of constant we are going to use *)
-let andb_prop = fun _ -> UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.andb_prop")
+let andb_prop = fun _ -> UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.bool.andb_prop")
 
 let andb_true_intro = fun _ ->
-  UnivGen.constr_of_global
+  UnivGen.constr_of_monomorphic_global
     (Coqlib.lib_ref "core.bool.andb_true_intro")
 
 (* We avoid to use lazy as the binding of constants can change *)
-let bb () = UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.type")
-let tt () = UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.true")
-let ff () = UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.false")
-let eq () = UnivGen.constr_of_global (Coqlib.lib_ref "core.eq.type")
+let bb () = UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.bool.type")
+let tt () = UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.bool.true")
+let ff () = UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.bool.false")
+let eq () = UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.eq.type")
 
-let sumbool () = UnivGen.constr_of_global (Coqlib.lib_ref "core.sumbool.type")
-let andb = fun _ -> UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.andb")
+let sumbool () = UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.sumbool.type")
+let andb = fun _ -> UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.bool.andb")
 
 let induct_on  c = induction false None c None None
 let destruct_on c = destruct false None c None None
@@ -873,7 +873,7 @@ let compute_dec_goal ind lnamesparrec nparrec =
         create_input (
           mkNamedProd n (mkFullInd ind (2*nparrec)) (
             mkNamedProd m (mkFullInd ind (2*nparrec+1)) (
-              mkApp(sumbool(),[|eqnm;mkApp (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.not.type",[|eqnm|])|])
+              mkApp(sumbool(),[|eqnm;mkApp (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.not.type",[|eqnm|])|])
           )
         )
       )
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 0ac97a74e4..fbf552e649 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -266,7 +266,7 @@ let eterm_obligations env name evm fs ?status t ty =
 
 let hide_obligation () =
   Coqlib.check_required_library ["Coq";"Program";"Tactics"];
-  UnivGen.constr_of_global (Coqlib.lib_ref "program.tactics.obligation")
+  UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "program.tactics.obligation")
 
 let pperror cmd = CErrors.user_err ~hdr:"Program" cmd
 let error s = pperror (str s)