Merge PR #10316: [lemmas] Reify info for implicits, universe decls, and rec theorems.

Reviewed-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: gares
Reviewed-by: ppedrot

1 files changed, 19 insertions, 1 deletions

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 51d90df89f..ab9df12766 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -13,13 +13,31 @@ Proof state:
 
   Proofs that are attached to a top-level constant (such as lemmas)
   are represented by `Lemmas.t`, as they do contain additional
-  information related to the constant declaration.
+  information related to the constant declaration. Some functions have
+  been renamed from `start_proof` to `start_lemma`
+
 
   Plugins that require access to the information about currently
   opened lemmas can add one of the `![proof]` attributes to their
   `mlg` entry, which will refine the type accordingly. See
   documentation in `vernacentries` for more information.
 
+  Proof `terminators` have been removed in favor of a principled
+  proof-saving path. This should not affect the regular API user, but
+  if plugin writes need special handling of the proof term they should
+  now work with Coq upstream to unsure the provided API does work and
+  is principled. Closing `hooks` are still available for simple
+  registration on constant save path, and essentially they do provide
+  the same power as terminators, but don't encourage their use other
+  than for simple tasks [such as adding a constant to a database]
+
+  Additionally, the API for proof/lemma handling has been refactored,
+  triples have been split into named arguments, and a few bits of
+  duplicated information among layers has been cleaned up. Most proof
+  information is now represented in a direct-style, as opposed to it
+  living inside closures in previous Coq versions; thus, proof
+  manipulation possibilities have been improved.
+
 ## Changes between Coq 8.9 and Coq 8.10
 
 ### ML4 Pre Processing