diff options
author | 2017-05-29 11:48:51 +0200 | |
---|---|---|
committer | 2017-05-29 11:58:48 +0200 | |
commit | fd7f056b155b2ebaafa3251a3c136117ebefc3e3 (patch) | |
tree | 46ff14eb398806485d148757a2f34e1889ef7aaf /dev/doc/changes.txt | |
parent | 4c1260299b707bd27765b0ab365092046b134a69 (diff) |
Cleanup: removal of constr_of_global.
Constrintern.pf_global returns a global_reference, not a constr,
adapt plugins accordingly, properly registering universes where
necessary.
Diffstat (limited to 'dev/doc/changes.txt')
-rw-r--r-- | dev/doc/changes.txt | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 7fad65bf0..92e3e8c9e 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -113,13 +113,17 @@ In Coqlib / reference location: We have removed from Coqlib functions returning `constr` from names. Now it is only possible to obtain references, that must be processed wrt the particular needs of the client. + We have changed in constrintern the functions returnin `constr` as + well to return global references instead. Users of `coq_constant/gen_constant` can do `Universes.constr_of_global (find_reference dir r)` _however_ note the warnings in the `Universes.constr_of_global` in the documentation. It is very likely that you were previously suffering from problems with polymorphic universes due to using - `Coqlib.coq_constant` that used to do this. + `Coqlib.coq_constant` that used to do this. You must rather use + `pf_constr_of_global` in tactics and `Evarutil.new_global` variants + when constructing terms in ML (see univpoly.txt for more information). ** Tactic API ** @@ -127,6 +131,10 @@ In Coqlib / reference location: Thus it only generates one instance of the global reference, and it is the caller's responsibility to perform a focus on the goal. +- pf_global, construct_reference, global_reference, + global_reference_in_absolute_module now return a global_reference + instead of a constr. + - The tclWEAK_PROGRESS and tclNOTSAMEGOAL tacticals were removed. Their usecase was very specific. Use tclPROGRESS instead. |