diff options
Diffstat (limited to 'dev/doc')
-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. |