diff options
| author | Emilio Jesus Gallego Arias | 2017-06-11 06:08:02 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-06-11 15:54:48 +0200 |
| commit | f610068823b33bdc0af752a646df05b98489d7ce (patch) | |
| tree | 5d664bd1b3efb43536250b30b0dffa724e28dba4 /vernac/command.ml | |
| parent | 79c42e22dd5106dcb85229ceec75331029ab5486 (diff) | |
[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`.
Diffstat (limited to 'vernac/command.ml')
| -rw-r--r-- | vernac/command.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |