diff options
| author | Matthieu Sozeau | 2018-10-12 18:15:16 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2018-10-18 14:18:24 +0200 |
| commit | e050884da17b260934a428d5b1bb11cd788ae0e1 (patch) | |
| tree | 579f4b8f99b7832d75ff2ead82ae209b41033ec0 /plugins/rtauto | |
| parent | 88ecdf6b51b0d7b4cde335cf94297c102d7d551e (diff) | |
[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.
Diffstat (limited to 'plugins/rtauto')
| -rw-r--r-- | plugins/rtauto/refl_tauto.ml | 8 |
1 files changed, 4 insertions, 4 deletions
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" |