From a506a219c15771b2bfe8a9a8ea1056feaea3eed8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 23 Nov 2000 14:07:55 +0000
Subject: 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
---
 proofs/pfedit.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

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 [< >])
-- 
cgit v1.2.3