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

5 files changed, 10 insertions, 10 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 10de3ab49..27b04eedb 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -270,7 +270,7 @@ let make_unfold (hintname, id) =
     (try 
        Declare.global_reference CCI id
      with Not_found -> 
-       errorlabstrm  "make_unfold" [<print_id id; 'sTR " not declared" >])
+       errorlabstrm  "make_unfold" [<pr_id id; 'sTR " not declared" >])
   in 
   (head_of_constr_reference hdconstr, 
    { hname = hintname;
@@ -489,7 +489,7 @@ let fmt_hint_id id =
     let c = Declare.global_reference CCI id in
     fmt_hint_list_for_head (head_of_constr_reference c)
   with Not_found -> 
-    [< print_id id; 'sTR " not declared" >]
+    [< pr_id id; 'sTR " not declared" >]
 
 (* Print all hints associated to head id in any database *)
 let print_hint_id id =  pPNL(fmt_hint_id id)
diff --git a/tactics/elim.ml b/tactics/elim.ml
index b92e949d5..34aab19ad 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -95,7 +95,7 @@ let inductive_of_ident gls id =
     | IsMutInd ity -> ity
     | _ ->
 	errorlabstrm "Decompose"
-	  [< print_id id; 'sTR " is not an inductive type" >]
+	  [< pr_id id; 'sTR " is not an inductive type" >]
 
 let decompose_these c l gls =
   let indl = List.map (inductive_of_ident gls) l in 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7d59ecf21..a90114641 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1361,7 +1361,7 @@ let general_rewrite_in lft2rgt id (c,lb) gls =
        let (_,ty) = lookup_named id (pf_env gls) in (body_of_type ty)
      with Not_found -> 
        errorlabstrm "general_rewrite_in" 
-	 [< 'sTR"No such hypothesis : "; print_id id >])
+	 [< 'sTR"No such hypothesis : "; pr_id id >])
   in
   let (wc,_) = startWalk gls
   and (_,_,t) = reduce_to_ind (pf_env gls) (project gls) (pf_type_of gls c) in
@@ -1380,7 +1380,7 @@ let general_rewrite_in lft2rgt id (c,lb) gls =
 		  (collapse_appl mbr_eq)) with
            | None ->
                errorlabstrm "general_rewrite_in" 
-		 [<'sTR "Nothing to rewrite in: "; print_id id>]
+		 [<'sTR "Nothing to rewrite in: "; pr_id id>]
            |Some (l2,nb_occ) ->
                (tclTHENSI 
 		  (tclTHEN 
@@ -1426,7 +1426,7 @@ let rewrite_in lR com id gls =
   (try 
      let _ = lookup_named id (pf_env gls) in () 
    with Not_found -> 
-     errorlabstrm "rewrite_in" [< 'sTR"No such hypothesis : " ;print_id id >]);
+     errorlabstrm "rewrite_in" [< 'sTR"No such hypothesis : " ;pr_id id >]);
   let c = pf_interp_constr gls com in
   let eqn = pf_type_of gls c in
   try
diff --git a/tactics/inv.ml b/tactics/inv.ml
index e2b2a0426..60b60ff6d 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -85,7 +85,7 @@ let make_inv_predicate env sigma ind id status concl =
       | Dep dflt_concl ->
 	  if not (dependent (mkVar id) concl) then
 	    errorlabstrm "make_inv_predicate"
-              [< 'sTR "Current goal does not depend on "; print_id id >];
+              [< 'sTR "Current goal does not depend on "; pr_id id >];
           (* We abstract the conclusion of goal with respect to
              realargs and c to * be concl in order to rewrite and have
              c also rewritten when the case * will be done *)
@@ -360,12 +360,12 @@ let not_found_message ids =
 
 let dep_prop_prop_message id =
   errorlabstrm "Inv"
-    [< 'sTR "Inversion on "; print_id id ;
+    [< 'sTR "Inversion on "; pr_id id ;
        'sTR " would needs dependent elimination Prop-Prop" >]
  
 let not_inductive_here id =
   errorlabstrm "mind_specif_of_mind"
-    [< 'sTR "Cannot recognize an inductive predicate in "; print_id id ;
+    [< 'sTR "Cannot recognize an inductive predicate in "; pr_id id ;
        'sTR ". If there is one, may be the structure of the arity or of the type of constructors is hidden by constant definitions." >]
 
 (* Noms d'errreurs obsolètes ?? *)
diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml
index b67bf13f8..b8bcb18ec 100644
--- a/tactics/wcclausenv.ml
+++ b/tactics/wcclausenv.ml
@@ -53,7 +53,7 @@ let clenv_constrain_with_bindings bl 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" >];
 		  clenv_lookup_name clause s
               | Nodep n ->