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/rtauto/refl_tauto.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'plugins/rtauto') 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" -- cgit v1.2.3