From c03d007ceeae5c2c5c835b03ce3dd2fb5be8212d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 28 Mar 2019 16:43:08 +0100
Subject: Fix top_printers after removal of imperative state

There's never a proof available in ocamldebug
I don't know about Drop.
---
 dev/top_printers.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 1f4f2246be..74be300134 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -60,7 +60,11 @@ let prrecarg = function
      str "Imbr[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]"
 let ppwf_paths x = pp (Rtree.pp_tree prrecarg x)
 
-let get_current_context = Vernacstate.Proof_global.get_current_context
+let get_current_context () =
+  try Vernacstate.Proof_global.get_current_context ()
+  with Vernacstate.Proof_global.NoCurrentProof ->
+    let env = Global.env() in
+    Evd.from_env env, env
 
 (* term printers *)
 let envpp pp = let sigma,env = get_current_context () in pp env sigma
-- 
cgit v1.2.3