From 3f99dcacdf94e77395913973c8ae5cf5b9c65b35 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 9 Jun 2019 14:10:45 +0200
Subject: [ci] Overlays for #10316

---
 dev/ci/user-overlays/10316-ejgallego-proof+recthms.sh | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 dev/ci/user-overlays/10316-ejgallego-proof+recthms.sh

(limited to 'dev')

diff --git a/dev/ci/user-overlays/10316-ejgallego-proof+recthms.sh b/dev/ci/user-overlays/10316-ejgallego-proof+recthms.sh
new file mode 100644
index 0000000000..d133bc9993
--- /dev/null
+++ b/dev/ci/user-overlays/10316-ejgallego-proof+recthms.sh
@@ -0,0 +1,18 @@
+if [ "$CI_PULL_REQUEST" = "10316" ] || [ "$CI_BRANCH" = "proof+recthms" ]; then
+
+    elpi_CI_REF=proof+recthms
+    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+    equations_CI_REF=proof+recthms
+    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+    mtac2_CI_REF=proof+recthms
+    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
+
+    paramcoq_CI_REF=proof+recthms
+    paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
+
+    quickchick_CI_REF=proof+recthms
+    quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick
+
+fi
-- 
cgit v1.2.3


From 6bed5c130c6368885967d1fdfd609bc72d708a7d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 21 Jun 2019 10:19:54 +0200
Subject: [proof] dev/doc/changes for the last refactorings

---
 dev/doc/changes.md | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

(limited to 'dev')

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
-- 
cgit v1.2.3