7 files changed, 70 insertions, 4 deletions
diff --git a/dev/base_include b/dev/base_include
index f764eaf4f5..b30bbaa3fa 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -142,7 +142,6 @@ open Ind_tables
 open Auto_ind_decl
 open Coqinit
 open Coqtop
-open Discharge
 open Himsg
 open Metasyntax
 open Mltop
@@ -209,3 +208,7 @@ let _ =
  print_string
    ("\n\tOcaml toplevel with Coq printers and utilities (use go();; to exit)\n\n");
  flush_all()
+
+(* Local Variables: *)
+(* mode: tuareg *)
+(* End: *)
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 818454dbbc..f07a5cdb98 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2019-06-11-V1"
+# CACHEKEY: "bionic_coq-V2019-06-21-V1"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -38,7 +38,7 @@ ENV COMPILER="4.05.0"
 # `num` does not have a version number as the right version to install varies
 # with the compiler version.
 ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.6.2 ounit.2.0.8 odoc.1.4.0" \
-    CI_OPAM="menhir.20181113 elpi.1.3.1 ocamlgraph.1.8.8"
+    CI_OPAM="menhir.20181113 elpi.1.4.0 ocamlgraph.1.8.8"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
 ENV COQIDE_OPAM="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5"
diff --git a/dev/ci/user-overlays/09645-ejgallego-proof+sayonara_baby.sh b/dev/ci/user-overlays/09645-ejgallego-proof+sayonara_baby.sh
new file mode 100644
index 0000000000..3029f3019c
--- /dev/null
+++ b/dev/ci/user-overlays/09645-ejgallego-proof+sayonara_baby.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "9645" ] || [ "$CI_BRANCH" = "proof+sayonara_baby" ]; then
+
+    equations_CI_REF=proof+sayonara_baby
+    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+    mtac2_CI_REF=proof+sayonara_baby
+    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
+
+    paramcoq_CI_REF=proof+sayonara_baby
+    paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
+
+fi
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
diff --git a/dev/ci/user-overlays/10406-ppedrot-desync-entry-proof.sh b/dev/ci/user-overlays/10406-ppedrot-desync-entry-proof.sh
new file mode 100644
index 0000000000..3122f953de
--- /dev/null
+++ b/dev/ci/user-overlays/10406-ppedrot-desync-entry-proof.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "10406" ] || [ "$CI_BRANCH" = "desync-entry-proof" ]; then
+
+    equations_CI_REF=desync-entry-proof
+    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+    quickchick_CI_REF=desync-entry-proof
+    quickchick_CI_GITURL=https://github.com/ppedrot/QuickChick
+
+fi
diff --git a/dev/ci/user-overlays/10416-gares-elpi-14.sh b/dev/ci/user-overlays/10416-gares-elpi-14.sh
new file mode 100644
index 0000000000..52d1005a7d
--- /dev/null
+++ b/dev/ci/user-overlays/10416-gares-elpi-14.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10416" ] || [ "$CI_BRANCH" = "elpi-14" ]; then
+
+    elpi_CI_REF="coq-master-elpi-14"
+    elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi
+
+fi
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