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