diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-02-19 11:12:52 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-19 11:12:52 +0100 |
commit | eaff61e0a19fcf6ebc2a9a8ae17327413274c67b (patch) | |
tree | acbbc416ad78bf8520893405c04855c600909576 /dev/doc | |
parent | 073b92396a68be30f77c80960a58ca562bb01f49 (diff) | |
parent | 68935660fbfdec2e357e123ed999073ed3b8fc26 (diff) |
Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`
Diffstat (limited to 'dev/doc')
-rw-r--r-- | dev/doc/changes.md | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md index aef62b009..16a31790a 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -20,6 +20,14 @@ General deprecation removed. Please, make sure your plugin is warning-free in 8.7 before trying to port it over 8.8. +Proof engine + + Due to the introduction of `EConstr` in 8.7, it is not necessary to + track "goal evar normal form status" anymore, thus the type `'a + Proofview.Goal.t` loses its ghost argument. This may introduce some + minor incompatibilities at the typing level. Code-wise, things + should remain the same. + We removed the following functions: - `Universes.unsafe_constr_of_global`: use `Global.constr_of_global_in_context` |