diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-23 14:07:55 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-23 14:07:55 +0000 |
| commit | a506a219c15771b2bfe8a9a8ea1056feaea3eed8 (patch) | |
| tree | f514864ea6aca7de66e5a88a6d1a45f9a73cbe94 /proofs | |
| parent | 95fdf37ed38d64c6358fcf8f5b841a56157db0b8 (diff) | |
print_id, print_sp -> pr_id, pr_sp
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@930 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index c883a5f27..0426955bc 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -36,7 +36,7 @@ let msg_proofs use_resume = match Edit.dom proof_edits with | [] -> [< 'sPC ; 'sTR"(No proof-editing in progress)." >] | l -> [< 'sTR"." ; 'fNL ; 'sTR"Proofs currently edited:" ; 'sPC ; - (prlist_with_sep pr_spc print_id (get_all_proof_names ())) ; + (prlist_with_sep pr_spc pr_id (get_all_proof_names ())) ; 'sTR"." ; (if use_resume then [< 'fNL ; 'sTR"Use \"Resume\" first." >] else [< >]) |