diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqloop.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 2 |
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 |