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

1 files changed, 6 insertions, 6 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 7fa6c5fee8..264cd139e1 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -98,20 +98,20 @@ let hypothesis_def_var is_refining ident n c =
 
 let minductive_message = function 
   | []  -> anomaly "no inductive definition"
-  | [x] -> [< print_id x; 'sTR " is defined">]
-  | l   -> hOV 0  [< prlist_with_sep pr_coma print_id l;
+  | [x] -> [< pr_id x; 'sTR " is defined">]
+  | l   -> hOV 0  [< prlist_with_sep pr_coma pr_id l;
 		     'sPC; 'sTR "are defined">]
 
 let recursive_message = function 
   | []  -> anomaly "no recursive definition"
-  | [x] -> [< print_id x; 'sTR " is recursively defined">]
-  | l   -> hOV 0 [< prlist_with_sep pr_coma print_id l;
+  | [x] -> [< pr_id x; 'sTR " is recursively defined">]
+  | l   -> hOV 0 [< prlist_with_sep pr_coma pr_id l;
 		    'sPC; 'sTR "are recursively defined">]
 
 let corecursive_message = function 
   | []  -> anomaly "no corecursive definition"
-  | [x] -> [< print_id x; 'sTR " is corecursively defined">]
-  | l   -> hOV 0 [< prlist_with_sep pr_coma print_id l;
+  | [x] -> [< pr_id x; 'sTR " is corecursively defined">]
+  | l   -> hOV 0 [< prlist_with_sep pr_coma pr_id l;
                     'sPC; 'sTR "are corecursively defined">]
 
 let build_mutual lparams lnamearconstrs finite =