From 7efaf86882488034e6545505e1eda7d6e1a6ce14 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 8 Apr 2018 09:35:26 +0200
Subject: [vernac] Adapt to removal of imperative proof state.

---
 toplevel/vernac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'toplevel/vernac.ml')

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index ef1dc6993b..ce584f1109 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -70,7 +70,7 @@ let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) =
 
       (* Force the command  *)
       let ndoc = if check then Stm.observe ~doc nsid else doc in
-      let new_proof = Proof_global.give_me_the_proof_opt () in
+      let new_proof = Vernacstate.Proof_global.give_me_the_proof_opt () in
       { state with doc = ndoc; sid = nsid; proof = new_proof; }
     with reraise ->
       (* XXX: In non-interactive mode edit_at seems to do very weird
-- 
cgit v1.2.3