diff options
-rw-r--r-- | library/goptions.ml | 2 | ||||
-rw-r--r-- | proofs/clenv.ml | 6 | ||||
-rw-r--r-- | proofs/logic.ml | 24 | ||||
-rw-r--r-- | proofs/tacmach.ml | 2 | ||||
-rw-r--r-- | tactics/auto.ml | 4 | ||||
-rw-r--r-- | tactics/elim.ml | 2 | ||||
-rw-r--r-- | tactics/equality.ml | 6 | ||||
-rw-r--r-- | tactics/inv.ml | 6 | ||||
-rw-r--r-- | tactics/wcclausenv.ml | 2 | ||||
-rw-r--r-- | toplevel/discharge.ml | 15 | ||||
-rw-r--r-- | toplevel/fhimsg.ml | 6 | ||||
-rw-r--r-- | toplevel/himsg.ml | 14 | ||||
-rw-r--r-- | toplevel/record.ml | 6 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 6 |
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") |