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.
---
 plugins/nsatz/nsatz.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/nsatz')

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