From e050884da17b260934a428d5b1bb11cd788ae0e1 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 12 Oct 2018 18:15:16 +0200
Subject: [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.
---
 proofs/tacmach.ml  | 5 ++++-
 proofs/tacmach.mli | 2 +-
 2 files changed, 5 insertions(+), 2 deletions(-)

(limited to 'proofs')

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
-- 
cgit v1.2.3