aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-06-11 06:08:02 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-06-11 15:54:48 +0200
commitf610068823b33bdc0af752a646df05b98489d7ce (patch)
tree5d664bd1b3efb43536250b30b0dffa724e28dba4 /toplevel
parent79c42e22dd5106dcb85229ceec75331029ab5486 (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 'toplevel')
-rw-r--r--toplevel/coqloop.ml2
-rw-r--r--toplevel/vernac.ml2
2 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 908786565..0b0ef6717 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -187,7 +187,7 @@ end
from cycling. *)
let make_prompt () =
try
- (Names.Id.to_string (Pfedit.get_current_proof_name ())) ^ " < "
+ (Names.Id.to_string (Proof_global.get_current_proof_name ())) ^ " < "
with Proof_global.NoCurrentProof ->
"Coq < "
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index a61ade784..d4146ace1 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -285,7 +285,7 @@ let ensure_exists f =
(* Compile a vernac file *)
let compile verbosely f =
let check_pending_proofs () =
- let pfs = Pfedit.get_all_proof_names () in
+ let pfs = Proof_global.get_all_proof_names () in
if not (List.is_empty pfs) then vernac_error (str "There are pending proofs")
in
match !Flags.compilation_mode with