diff options
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 c883a5f270..0426955bce 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 [< >]) |