From f610068823b33bdc0af752a646df05b98489d7ce Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 11 Jun 2017 06:08:02 +0200
Subject: [proof] Deprecate redundant wrappers.

As we would like to reduce the role of proof_global in future
versions, we start to deprecate old compatibility aliases in `Pfedit`
in favor of the real functions underlying the 8.5 proof engine.

We also deprecate a couple of alias types and explicitly mark the few
remaining uses of `Pfedit`.
---
 vernac/command.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac/command.ml')

diff --git a/vernac/command.ml b/vernac/command.ml
index b1425d7034..998e7803e1 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -187,7 +187,7 @@ let declare_definition ident (local, p, k) ce pl imps hook =
     let () = definition_message ident in
     let gr = VarRef ident in
     let () = maybe_declare_manual_implicits false gr imps in
-    let () = if Pfedit.refining () then
+    let () = if Proof_global.there_are_pending_proofs () then
 	       warn_definition_not_visible ident
     in
     gr
@@ -233,7 +233,7 @@ match local with
   let _ = declare_variable ident decl in
   let () = assumption_message ident in
   let () =
-    if not !Flags.quiet && Pfedit.refining () then
+    if not !Flags.quiet && Proof_global.there_are_pending_proofs () then
     Feedback.msg_info (str"Variable" ++ spc () ++ pr_id ident ++
     strbrk " is not visible from current goals")
   in
-- 
cgit v1.2.3