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/firstorder/rules.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'plugins/firstorder')

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