From 6b61b63bb8626827708024cbea1312a703a54124 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 6 Sep 2018 20:26:03 +0200
Subject: [engine] Remove and deprecate `nf_enter` et al.

After the introduction of `EConstr`, "normalization" has become
unnecessary, we thus deprecate the `nf_*` family of functions.

Test-suite and CI pass after the fix for #8513.
---
 dev/doc/changes.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev/doc/changes.md')

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 1eea2443fe..4f3d793ed4 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -219,7 +219,7 @@ General deprecation
 
 Proof engine
 
-  Due to the introduction of `EConstr` in 8.7, it is not necessary to
+- 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
-- 
cgit v1.2.3