diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-14 18:16:31 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-14 18:16:31 +0200 |
| commit | cb41d7b40c401c15e9cb66f508f89dbd1bdcdbff (patch) | |
| tree | f852248c2ce2be0cc3e6aae136e961561e395e85 /toplevel | |
| parent | e70bec8fba8b15155aca41812225fcf42e1408e0 (diff) | |
| parent | f610068823b33bdc0af752a646df05b98489d7ce (diff) | |
Merge PR#763: [proof] Deprecate redundant wrappers.
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 |