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, 23 insertions, 24 deletions

diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 3c702e2b4e..6e79134bb9 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 4f60a710c0..442735ddf0 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 afaf5a2d4a..aa4f719c55 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 d377b46e8c..b127159b19 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 6363decfe1..8bf20ca694 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")