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

14 files changed, 50 insertions, 51 deletions

diff --git a/library/goptions.ml b/library/goptions.ml
index 64b08f6f4..dc5f994e3 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -340,7 +340,7 @@ let msg_sync_option_value (name,v) =
     | BoolValue false -> [< 'sTR "false" >]
     | IntValue n      -> [< 'iNT n >]
     | StringValue s   -> [< 'sTR s >]
-    | IdentValue id    -> [< print_id id >]
+    | IdentValue id    -> [< pr_id id >]
 
 let msg_async_option_value (name,vref) =
   match vref with
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 >]
 
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 ->
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 3c702e2b4..6e79134bb 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -101,16 +101,16 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
 (* Discharge messages. *)
 
 let constant_message id =
-  if Options.is_verbose() then pPNL [< print_id id; 'sTR " is discharged." >]
+  if Options.is_verbose() then pPNL [< pr_id id; 'sTR " is discharged." >]
 
 let inductive_message inds =
   if Options.is_verbose() then 
     pPNL (hOV 0 
 	    (match inds with
 	       | [] -> assert false
-	       | [(i,_,_,_)] -> [< print_id i; 'sTR " is discharged." >]
+	       | [(i,_,_,_)] -> [< pr_id i; 'sTR " is discharged." >]
 	       | l -> [< prlist_with_sep pr_coma 
-			   (fun (id,_,_,_) -> print_id id) l;
+			   (fun (id,_,_,_) -> pr_id id) l;
 			 'sPC; 'sTR "are discharged.">]))
 
 (* Discharge operations for the various objects of the environment. *)
@@ -122,8 +122,7 @@ type discharge_operation =
   | Inductive of mutual_inductive_entry * bool
   | Class of cl_typ * cl_info_typ
   | Struc of inductive_path * struc_typ
-  | Coercion of ((coe_typ * coe_info_typ) * cl_typ * cl_typ) 
-              * identifier * int 
+  | Coercion of ((coe_typ * coe_info_typ) * cl_typ * cl_typ)
 
 (* Main function to traverse the library segment and compute the various
    discharge operations. *)
@@ -192,8 +191,8 @@ let process_object oldenv dir sec_sp
         if coeinfo.cOE_STRE = (DischargeAt sec_sp) then 
 	  (ops,ids_to_discard,work_alist)
         else
-	  let (y,idf,ps) = process_coercion sec_sp x in
-          ((Coercion (y,idf,ps))::ops, ids_to_discard, work_alist)
+	  let y = process_coercion sec_sp x in
+          ((Coercion y)::ops, ids_to_discard, work_alist)
                     
     | "STRUCTURE" ->
 	let ((sp,i),info) = outStruc lobj in
@@ -236,7 +235,7 @@ let process_operation = function
       Lib.add_anonymous_leaf (inClass (y1,y2))
   | Struc (newsp,strobj) ->
       Lib.add_anonymous_leaf (inStruc (newsp,strobj))
-  | Coercion ((_,_,clt) as y,idf,ps) ->
+  | Coercion y ->
       Lib.add_anonymous_leaf (inCoercion y) 
 
 let push_inductive_names ccitab sp mie =
diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml
index 4f60a710c..442735ddf 100644
--- a/toplevel/fhimsg.ml
+++ b/toplevel/fhimsg.ml
@@ -19,13 +19,13 @@ module Make = functor (P : Printer) -> struct
 
   let print_decl k env (s,typ) =
     let ptyp = P.pr_term k env (body_of_type typ) in 
-    [< 'sPC; print_id s; 'sTR" : "; ptyp >]
+    [< 'sPC; pr_id s; 'sTR" : "; ptyp >]
   
   let print_binding k env = function
     | Anonymous,ty -> 
 	[< 'sPC; 'sTR"_" ; 'sTR" : " ; P.pr_term k env (body_of_type ty) >]
     | Name id,ty -> 
-	[< 'sPC; print_id id ; 'sTR" : "; P.pr_term k env (body_of_type ty) >]
+	[< 'sPC; pr_id id ; 'sTR" : "; P.pr_term k env (body_of_type ty) >]
 
 (****
   let sign_it_with f sign e =
@@ -78,7 +78,7 @@ let explain_bad_assumption k ctx c =
      'bRK(1,1); pc; 'sPC; 'sTR "because this term is not a type." >];;
 
 let explain_reference_variables id =
-  [< 'sTR "the constant"; 'sPC; print_id id; 'sPC; 
+  [< 'sTR "the constant"; 'sPC; pr_id id; 'sPC; 
      'sTR "refers to variables which are not in the context" >]
 
 let msg_bad_elimination ctx k = function
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index afaf5a2d4..aa4f719c5 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -39,7 +39,7 @@ let explain_bad_assumption k ctx c =
      'bRK(1,1); pc; 'sPC; 'sTR "because this term is not a type." >];;
 
 let explain_reference_variables id =
-  [< 'sTR "the constant"; 'sPC; print_id id; 'sPC; 
+  [< 'sTR "the constant"; 'sPC; pr_id id; 'sPC; 
      'sTR "refers to variables which are not in the context" >]
 
 let msg_bad_elimination ctx k = function
@@ -280,7 +280,7 @@ let explain_var_not_found k ctx id =
      'sPC ; 'sTR "in the current"; 'sPC ; 'sTR "environment" >]
 
 let explain_global_not_found k ctx q = 
-  [< 'sTR "The reference"; 'sPC; print_qualid q;
+  [< 'sTR "The reference"; 'sPC; pr_qualid q;
      'sPC ; 'sTR "was not found"; 
      'sPC ; 'sTR "in the current"; 'sPC ; 'sTR "environment" >]
 
@@ -458,16 +458,16 @@ let error_bad_ind_parameters k env c n v1 v2  =
      'sTR "must be "; pv1; 'sTR " in"; 'bRK(1,1); pc >]
 
 let error_same_names_types id =
-  [< 'sTR "The name"; 'sPC; print_id id; 'sPC; 
+  [< 'sTR "The name"; 'sPC; pr_id id; 'sPC; 
      'sTR "is used twice is the inductive types definition." >]
 
 let error_same_names_constructors id cid =
-  [< 'sTR "The constructor name"; 'sPC; print_id cid; 'sPC; 
+  [< 'sTR "The constructor name"; 'sPC; pr_id cid; 'sPC; 
      'sTR "is used twice is the definition of type"; 'sPC;
-     print_id id >]
+     pr_id id >]
 
 let error_not_an_arity id =
-  [< 'sTR "The type of"; 'sPC; print_id id; 'sPC; 'sTR "is not an arity." >]
+  [< 'sTR "The type of"; 'sPC; pr_id id; 'sPC; 'sTR "is not an arity." >]
 
 let error_bad_entry () =
   [< 'sTR "Bad inductive definition." >]
@@ -480,7 +480,7 @@ let error_not_allowed_case_analysis dep kind i =
 
 let error_bad_induction dep indid kind =
   [<'sTR (if dep then "Dependent" else "Non dependend");
-    'sTR " induction for type "; print_id indid;
+    'sTR " induction for type "; pr_id indid;
     'sTR " and sort "; print_sort kind; 
     'sTR "is not allowed">]
 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index d377b46e8..b127159b1 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -62,8 +62,8 @@ let all_vars t =
   in 
   aux(t,[]) 
    
-let print_id_list l = 
-  [< 'sTR "[" ; prlist_with_sep pr_coma print_id l; 'sTR "]" >]
+let pr_id_list l = 
+  [< 'sTR "[" ; prlist_with_sep pr_coma pr_id l; 'sTR "]" >]
 
 open Environ
 
@@ -125,7 +125,7 @@ let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) =
 	   (warning_or_error coe
               [< 'sTR(string_of_id fi);
 		 'sTR" cannot be defined because the projection"; 'sTR s; 'sPC;
-                 prlist_with_sep pr_coma print_id bad_projs;
+                 prlist_with_sep pr_coma pr_id bad_projs;
 		 'sPC; 'sTR have; 'sTR "n't." >]);
            (None::sp_projs,fi::ids_not_ok,subst)
          end else 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 6363decfe..8bf20ca69 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -633,7 +633,7 @@ let _ =
     (function [] ->
        (fun () ->
 	  let l = Pfedit.get_all_proof_names() in 
-	  mSGNL (prlist_with_sep pr_spc print_id l))
+	  mSGNL (prlist_with_sep pr_spc pr_id l))
        | _  -> bad_vernac_args "ShowProofs")
 
 let _ =
@@ -753,14 +753,14 @@ let _ =
 		  ()
               with e ->
             	if is_unsafe "proof" then begin
-                  mSGNL [< 'sTR"Error: checking of theorem " ; print_id s ;
+                  mSGNL [< 'sTR"Error: checking of theorem " ; pr_id s ;
                            'sPC ; 'sTR"failed" ;
                            'sTR"... converting to Axiom" >];
                   delete_proof s;
                   parameter_def_var (string_of_id s) com
            	end else 
 		  errorlabstrm "vernacentries__TheoremProof"
-                    [< 'sTR"checking of theorem " ; print_id s ; 'sPC ;
+                    [< 'sTR"checking of theorem " ; pr_id s ; 'sPC ;
                        'sTR"failed... aborting" >])
        | _ -> bad_vernac_args "TheoremProof")