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

5 files changed, 12 insertions, 12 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 17b411f9f7..87d9e306fe 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -368,7 +368,7 @@ let import_constraints g sp cst =
     merge_constraints cst g
   with UniverseInconsistency ->
     errorlabstrm "import_constraints"
-      [< 'sTR "Universe Inconsistency during import of"; 'sPC; print_sp sp >]
+      [< 'sTR "Universe Inconsistency during import of"; 'sPC; pr_sp sp >]
 
 let import cenv env =
   check_imports env cenv.cenv_needed;
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index cfd2d919c6..1edeb78f8f 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -424,7 +424,7 @@ let rec substlin env name n ol c =
           with
 	      NotEvaluableConst _ ->
 		errorlabstrm "substlin"
-		  [< print_sp sp; 'sTR " is not a defined constant" >]
+		  [< pr_sp sp; 'sTR " is not a defined constant" >]
         else 
 	  ((n+1),ol,c)
 
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 [< >])
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 =