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

2 files changed, 9 insertions, 9 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 =
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
index 1807d96356..e4b1706542 100644
--- a/toplevel/minicoq.ml
+++ b/toplevel/minicoq.ml
@@ -47,19 +47,19 @@ let definition id ty c =
   let ce = { const_entry_body = Cooked c; const_entry_type = ty } in
   let sp = make_path [] id CCI in
   env := add_constant sp ce !env;
-  mSGNL (hOV 0 [< print_id id; 'sPC; 'sTR"is defined"; 'fNL >])
+  mSGNL (hOV 0 [< pr_id id; 'sPC; 'sTR"is defined"; 'fNL >])
 
 let parameter id t =
   let t = globalize [] t in
   let sp = make_path [] id CCI in
   env := add_parameter sp t !env;
-  mSGNL (hOV 0 [< 'sTR"parameter"; 'sPC; print_id id; 
+  mSGNL (hOV 0 [< 'sTR"parameter"; 'sPC; pr_id id; 
 		  'sPC; 'sTR"is declared"; 'fNL >])
 
 let variable id t =
   let t = globalize [] t in
   env := push_named_assum (id,t) !env;
-  mSGNL (hOV 0 [< 'sTR"variable"; 'sPC; print_id id; 
+  mSGNL (hOV 0 [< 'sTR"variable"; 'sPC; pr_id id; 
 		  'sPC; 'sTR"is declared"; 'fNL >])
 
 let put_DLAMSV lna lc =