From 68935660fbfdec2e357e123ed999073ed3b8fc26 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 11 Feb 2018 16:00:04 +0100
Subject: [engine] Remove ghost parameter from `Proofview.Goal.t`

In current code, `Proofview.Goal.t` uses a phantom type to indicate
whether the goal was properly substituted wrt current `evar_map` or
not.

After the introduction of `EConstr`, this distinction should have
become unnecessary, thus we remove the phantom parameter from
`'a Proofview.Goal.t`. This may introduce some minor incompatibilities
at the typing level. Code-wise, things should remain the same.

We thus deprecate `assume`. In a next commit, we will remove
normalization as much as possible from the code.
---
 dev/doc/changes.md | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'dev')

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index aef62b0092..16a31790a4 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`
-- 
cgit v1.2.3