diff options
author | 2017-05-24 19:57:06 +0200 | |
---|---|---|
committer | 2017-05-27 20:27:38 +0200 | |
commit | 5cc13770ac2358d583b21f217b8c65d2d5abd850 (patch) | |
tree | b4efff0efa2bb11c8586dbff2ef85d4d8d0328dd /dev/doc/changes.txt | |
parent | 6841c6db48d57911d3886057e1ca47a5aa161ca7 (diff) |
[coqlib] Move `Coqlib` to `library/`.
We move Coqlib to library in preparation for the late binding of
Gallina-level references. Placing `Coqlib` in `library/` is convenient
as some components such as pretyping need to depend on it.
By moving we lose the ability to locate references by syntactic
abbreviations, but IMHO it makes to require ML code to refer to
a true constant instead of an abbreviation/notation.
Unfortunately this change means that we break the `Coqlib`
API (providing a compatibility function is not possible), however we
do so for a good reason.
The main changes are:
- move `Coqlib` to `library/`.
- remove reference -> term from `Coqlib`. In particular, clients will
have different needs with regards to universes/evar_maps, so we
force them to call the (not very safe) `Universes.constr_of_global`
explicitly so the users are marked.
- move late binding of impossible case from `Termops` to
`pretying/Evarconv`. Remove hook.
- `Coqlib.find_reference` doesn't support syntactic abbreviations
anymore.
- remove duplication of `Coqlib` code in `Program`.
- remove duplication of `Coqlib` code in `Ltac.Rewrite`.
- A special note about bug 5066 and commit 6e87877 . This case
illustrates the danger of duplication in the code base; the solution
chosen there was to transform the not-found anomaly into an error
message, however the general policy was far from clear. The long
term solution is indeed make `find_reference` emit `Not_found` and
let the client handle the error maybe non-fatally. (so they can test
for constants.
Diffstat (limited to 'dev/doc/changes.txt')
-rw-r--r-- | dev/doc/changes.txt | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index d52c18462..bb6c2f660 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -108,6 +108,19 @@ In GOption: passed to workers, etc... As a consequence, the field `Goptions.optsync` has been removed. +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. + + 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. + ** Tactic API ** - pf_constr_of_global now returns a tactic instead of taking a continuation. |