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`. --- toplevel/coqloop.ml | 2 +- toplevel/vernac.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'toplevel') 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 -- cgit v1.2.3