From 0c748e670ef1a81cb35c1cc55892dba141c25930 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 2 Apr 2020 01:41:20 -0400
Subject: [proof] Merge `Proof_global` into `Declare`

We place creation and saving of interactive proofs in the same module;
this will allow to make `proof_entry` private, improving invariants
and control over clients, and to reduce the API [for example next
commit will move abstract declaration into this module, removing the
exported ad-hoc `build_constant_by_tactic`]

Next step will be to unify all the common code in the interactive /
non-interactive case; but we need to tweak the handling of obligations
first.
---
 dev/top_printers.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 7002cbffac..542893ad0b 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -59,8 +59,8 @@ let prrecarg = function
 let ppwf_paths x = pp (Rtree.pp_tree prrecarg x)
 
 let get_current_context () =
-  try Vernacstate.Proof_global.get_current_context ()
-  with Vernacstate.Proof_global.NoCurrentProof ->
+  try Vernacstate.Declare.get_current_context ()
+  with Vernacstate.Declare.NoCurrentProof ->
     let env = Global.env() in
     Evd.from_env env, env
   [@@ocaml.warning "-3"]
-- 
cgit v1.2.3


From b87b27011a061ead6eca7d8630ad3f59c45877e2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 2 Apr 2020 01:54:29 -0400
Subject: [dev] [doc] Changes.

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

(limited to 'dev')

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index eac8d86b0a..9498ab8bbb 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -9,6 +9,13 @@
 
 ### ML API
 
+Proof state and constant declaration:
+
+- A large consolidation of the API handling interactive and
+  non-interactive constant has been performed; low-level APIs are no
+  longer available, and the functionality of the `Proof_global` module
+  has been merged into `Declare`.
+
 Notations:
 
 - Most operators on numerals have moved to file numTok.ml.
@@ -68,7 +75,6 @@ Proof state:
   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
-- 
cgit v1.2.3