From 901f1b200feea81c3c9129b153dce067e41b9770 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 6 Nov 2000 22:01:12 +0000
Subject: Nettoyage Names et conséquences (dont ajout d'un type dir_path,
 argument de DischargeAt)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@811 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/pfedit.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index d12a65db61..c883a5f270 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -36,7 +36,8 @@ 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 ;
-               (print_idl (get_all_proof_names ())) ; 'sTR"." ;
+               (prlist_with_sep pr_spc print_id (get_all_proof_names ())) ;
+	       'sTR"." ;
                (if use_resume then [< 'fNL ; 'sTR"Use \"Resume\" first." >]
               	else [< >])
             >]
-- 
cgit v1.2.3