print_id, print_sp -> pr_id, pr_sp

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@923 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 16 insertions, 16 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index daef42298..1332e0ecd 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -850,7 +850,7 @@ let clenv_lookup_name clenv id =
   match intmap_inv clenv.namenv id with
     | []  -> 
 	errorlabstrm "clenv_lookup_name"
-          [< 'sTR"No such bound variable "; print_id id >]
+          [< 'sTR"No such bound variable "; pr_id id >]
     | [n] -> 
 	n
     |  _  -> 
@@ -869,7 +869,7 @@ let clenv_match_args s clause =
              | Dep s ->
 		 if List.mem_assoc b t then 
 		   errorlabstrm "clenv_match_args" 
-		     [< 'sTR "The variable "; print_id s; 
+		     [< 'sTR "The variable "; pr_id s; 
 			'sTR " occurs more than once in binding" >]
 		 else 
 		   clenv_lookup_name clause s
@@ -1027,7 +1027,7 @@ let pr_clenv clenv =
   let pr_name mv =
     try 
       let id = Intmap.find mv clenv.namenv in
-      [< 'sTR"[" ; print_id id ; 'sTR"]" >]
+      [< 'sTR"[" ; pr_id id ; 'sTR"]" >]
     with Not_found -> [< >]
   in
   let pr_meta_binding = function
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 0e7b5dc53..8021f336e 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -548,36 +548,36 @@ open Printer
 
 let pr_prim_rule = function
   | {name=Intro;newids=[id]} -> 
-      [< 'sTR"Intro " ; print_id id >]
+      [< 'sTR"Intro " ; pr_id id >]
 	
   | {name=Intro_after;newids=[id]} -> 
-      [< 'sTR"intro after " ; print_id id >]
+      [< 'sTR"intro after " ; pr_id id >]
 	
   | {name=Intro_replacing;newids=[id]} -> 
-      [< 'sTR"intro replacing " ; print_id id >]
+      [< 'sTR"intro replacing " ; pr_id id >]
 	
   | {name=Fix;newids=[f];params=[Num(_,n)]} -> 
-      [< 'sTR"Fix "; print_id f; 'sTR"/"; 'iNT n>]
+      [< 'sTR"Fix "; pr_id f; 'sTR"/"; 'iNT n>]
       
   | {name=Fix;newids=(f::lf);params=(Num(_,n))::ln;terms=lar} -> 
       let rec print_mut = 
         function (f::lf),((Num(_,n))::ln),(ar::lar) -> 
-          [< print_id f; 'sTR"/"; 'iNT n; 'sTR" : "; prterm ar;
+          [< pr_id f; 'sTR"/"; 'iNT n; 'sTR" : "; prterm ar;
              print_mut (lf,ln,lar)>]
           | _ -> [<>] in
-      [< 'sTR"Fix "; print_id f; 'sTR"/"; 'iNT n;
+      [< 'sTR"Fix "; pr_id f; 'sTR"/"; 'iNT n;
          'sTR" with "; print_mut (lf,ln,lar) >]
       
   | {name=Cofix;newids=[f];terms=[]} -> 
-      [< 'sTR"Cofix "; print_id f >]
+      [< 'sTR"Cofix "; pr_id f >]
       
   | {name=Cofix;newids=(f::lf);terms=lar} -> 
       let rec print_mut = 
         function (f::lf),(ar::lar) -> 
-	  [< print_id f; 'sTR" : "; prterm ar; print_mut (lf,lar)>]
+	  [< pr_id f; 'sTR" : "; prterm ar; print_mut (lf,lar)>]
           | _ -> [<>] 
       in
-      [< 'sTR"Cofix "; print_id f;  'sTR" with "; print_mut (lf,lar) >]
+      [< 'sTR"Cofix "; pr_id f;  'sTR" with "; print_mut (lf,lar) >]
 
   | {name=Refine;terms=[c]} -> 
       [< 'sTR(if occur_meta c then "Refine " else "Exact ") ; prterm c >]
@@ -586,13 +586,13 @@ let pr_prim_rule = function
       [< 'sTR"Change " ; prterm c >]
       
   | {name=Convert_hyp;hypspecs=[id];terms=[c]} ->
-      [< 'sTR"Change " ; prterm c ; 'sPC ; 'sTR"in " ; print_id id >]
+      [< 'sTR"Change " ; prterm c ; 'sPC ; 'sTR"in " ; pr_id id >]
       
   | {name=Thin;hypspecs=ids} ->
-      [< 'sTR"Clear " ; prlist_with_sep pr_spc print_id ids >]
+      [< 'sTR"Clear " ; prlist_with_sep pr_spc pr_id ids >]
       
   | {name=Move withdep;hypspecs=[id1;id2]} ->
       [< 'sTR (if withdep then "Dependent " else "");
-	 'sTR"Move " ; print_id id1; 'sTR " after "; print_id id2 >]
+	 'sTR"Move " ; pr_id id1; 'sTR " after "; pr_id id2 >]
       
   | _ -> anomaly "pr_prim_rule: Unrecognized primitive rule"
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 272fe6eae..575b18930 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -513,7 +513,7 @@ let pr_com sigma goal com =
             (Astterm.interp_constr sigma (Evarutil.evar_env goal) com))
 
 let pr_one_binding sigma goal = function
-  | (Dep id,com)  -> [< print_id id ; 'sTR":=" ; pr_com sigma goal com >]
+  | (Dep id,com)  -> [< pr_id id ; 'sTR":=" ; pr_com sigma goal com >]
   | (NoDep n,com) -> [< 'iNT n ; 'sTR":=" ; pr_com sigma goal com >]
   | (Com,com)     -> [< pr_com sigma goal com >]