From 5a39e6c08d428d774165e0ef3922ba8b75eee9e1 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Mon, 28 Jan 2013 21:05:35 +0000 Subject: Uniformization of the "anomaly" command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/cc/ccalgo.ml | 18 +++++------ plugins/cc/ccproof.ml | 4 +-- plugins/decl_mode/decl_interp.ml | 6 ++-- plugins/decl_mode/decl_proof_instr.ml | 42 +++++++++++++------------- plugins/decl_mode/g_decl_mode.ml4 | 6 ++-- plugins/decl_mode/ppdecl_proof.ml | 6 ++-- plugins/extraction/extract_env.ml | 2 +- plugins/extraction/modutil.ml | 4 +-- plugins/extraction/table.ml | 2 +- plugins/firstorder/instances.ml | 4 +-- plugins/firstorder/rules.ml | 2 +- plugins/funind/functional_principles_proofs.ml | 18 +++++------ plugins/funind/functional_principles_types.ml | 6 ++-- plugins/funind/glob_term_to_relation.ml | 2 +- plugins/funind/glob_termops.ml | 4 +-- plugins/funind/indfun.ml | 10 +++--- plugins/funind/indfun_common.ml | 4 +-- plugins/funind/invfun.ml | 16 +++++----- plugins/funind/recdef.ml | 22 +++++++------- plugins/micromega/g_micromega.ml4 | 2 +- plugins/omega/coq_omega.ml | 4 +-- plugins/quote/quote.ml | 2 +- plugins/rtauto/proof_search.ml | 10 +++--- plugins/xml/acic2Xml.ml4 | 2 +- plugins/xml/cic2acic.ml | 18 ++++++----- plugins/xml/xmlcommand.ml | 6 ++-- 26 files changed, 112 insertions(+), 110 deletions(-) (limited to 'plugins') diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 21077ecc8..a85c80a79 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -51,7 +51,7 @@ module ST=struct let enter t sign st= if Hashtbl.mem st.toterm sign then - anomaly "enter: signature already entered" + anomaly ~label:"enter" (Pp.str "signature already entered") else Hashtbl.replace st.toterm sign t; Hashtbl.replace st.tosign t sign @@ -272,7 +272,7 @@ let find uf i= find_aux uf [] i let get_representative uf i= match uf.map.(i).clas with Rep r -> r - | _ -> anomaly "get_representative: not a representative" + | _ -> anomaly ~label:"get_representative" (Pp.str "not a representative") let find_pac uf i pac = PacMap.find pac (get_representative uf i).constructors @@ -280,7 +280,7 @@ let find_pac uf i pac = let get_constructor_info uf i= match uf.map.(i).term with Constructor cinfo->cinfo - | _ -> anomaly "get_constructor: not a constructor" + | _ -> anomaly ~label:"get_constructor" (Pp.str "not a constructor") let size uf i= (get_representative uf i).weight @@ -325,7 +325,7 @@ let term uf i=uf.map.(i).term let subterms uf i= match uf.map.(i).vertex with Node(j,k) -> (j,k) - | _ -> anomaly "subterms: not a node" + | _ -> anomaly ~label:"subterms" (Pp.str "not a node") let signature uf i= let j,k=subterms uf i in (find uf j,find uf k) @@ -402,7 +402,7 @@ let rec canonize_name c = let build_subst uf subst = Array.map (fun i -> try term uf i - with _ -> anomaly "incomplete matching") subst + with _ -> anomaly (Pp.str "incomplete matching")) subst let rec inst_pattern subst = function PVar i -> @@ -657,8 +657,8 @@ let process_constructor_mark t i rep pac state = {lhs=s1;rhs=s2;rule=Injection(s,opac,t,pac,n)} state.combine; f (n-1) q1 q2 - | _-> anomaly - "add_pacs : weird error in injection subterms merge" + | _-> anomaly ~label:"add_pacs" + (Pp.str "weird error in injection subterms merge") in f cinfo.ci_nhyps opac.args pac.args | Partial_applied | Partial _ -> add_pac rep pac t; @@ -750,7 +750,7 @@ let complete_one_class state i= let ct = app (term state.uf i) typ pac.arity in state.uf.epsilons <- pac :: state.uf.epsilons; ignore (add_term state ct) - | _ -> anomaly "wrong incomplete class" + | _ -> anomaly (Pp.str "wrong incomplete class") let complete state = Int.Set.iter (complete_one_class state) state.pa_classes @@ -890,7 +890,7 @@ let find_instances state = check_for_interrupt (); do_match state res pb_stack done; - anomaly "get out of here !" + anomaly (Pp.str "get out of here !") with Stack.Empty -> () in !res diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index 25c01f2bd..5244dcf17 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -47,7 +47,7 @@ let rec ptrans p1 p3= {p_lhs=p1.p_lhs; p_rhs=p3.p_rhs; p_rule=Trans (p1,p3)} - else anomaly "invalid cc transitivity" + else anomaly (Pp.str "invalid cc transitivity") let rec psym p = match p.p_rule with @@ -85,7 +85,7 @@ let rec nth_arg t n= if n>0 then nth_arg t1 (n-1) else t2 - | _ -> anomaly "nth_arg: not enough args" + | _ -> anomaly ~label:"nth_arg" (Pp.str "not enough args") let pinject p c n a = {p_lhs=nth_arg p.p_lhs (n-a); diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index eb7d9e8e4..3cc0686ad 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -237,7 +237,7 @@ let rec deanonymize ids = let rec glob_of_pat = function - PatVar (loc,Anonymous) -> anomaly "Anonymous pattern variable" + PatVar (loc,Anonymous) -> anomaly (Pp.str "Anonymous pattern variable") | PatVar (loc,Name id) -> GVar (loc,id) | PatCstr(loc,((ind,_) as cstr),lpat,_) -> @@ -288,10 +288,10 @@ let bind_aliases patvars subst patt = let interp_pattern env pat_expr = let patvars,pats = Constrintern.intern_pattern env pat_expr in match pats with - [] -> anomaly "empty pattern list" + [] -> anomaly (Pp.str "empty pattern list") | [subst,patt] -> (patvars,bind_aliases patvars subst patt,patt) - | _ -> anomaly "undetected disjunctive pattern" + | _ -> anomaly (Pp.str "undetected disjunctive pattern") let rec match_args dest names constr = function [] -> [],names,substl names constr diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index a42e0cb3e..c25a150f4 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -177,7 +177,7 @@ let close_block bt pts = ET_Case_analysis -> error "\"end cases\" expected." | ET_Induction -> error "\"end induction\" expected." end - | _,_ -> anomaly "Lonely suppose on stack." + | _,_ -> anomaly (Pp.str "Lonely suppose on stack.") (* utility for suppose / suppose it is *) @@ -187,7 +187,7 @@ let close_previous_case pts = Proof.is_done pts then match get_top_stack pts with - Per (et,_,_,_) :: _ -> anomaly "Weird case occured ..." + Per (et,_,_,_) :: _ -> anomaly (Pp.str "Weird case occured ...") | Suppose_case :: Per (et,_,_,_) :: _ -> goto_current_focus (pts) | _ -> error "Not inside a proof per cases or induction." @@ -233,7 +233,7 @@ let prepare_goal items gls = filter_hyps (let keep = !tokeep in fun id -> Id.Set.mem id keep)] gls let my_automation_tac = ref - (fun gls -> anomaly "No automation registered") + (fun gls -> anomaly (Pp.str "No automation registered")) let register_automation_tac tac = my_automation_tac:= tac @@ -380,7 +380,7 @@ let concl_refiner metas body gls = let env = pf_env gls in let sort = family_of_sort (Typing.sort_of env evd concl) in let rec aux env avoid subst = function - [] -> anomaly "concl_refiner: cannot happen" + [] -> anomaly ~label:"concl_refiner" (Pp.str "cannot happen") | (n,typ)::rest -> let _A = subst_meta subst typ in let x = id_of_name_using_hdchar env _A Anonymous in @@ -896,7 +896,7 @@ let register_nodep_subcase id= function | EK_nodep -> clauses,Per(et,pi,EK_nodep,id::clauses)::s | EK_dep _ -> error "Do not mix \"suppose\" with \"suppose it is\"." end - | _ -> anomaly "wrong stack state" + | _ -> anomaly (Pp.str "wrong stack state") let suppose_tac hyps gls0 = let info = get_its_info gls0 in @@ -950,7 +950,7 @@ let rec add_branch ((id,_) as cpl) pats tree= match tree with End_patt cpl0 -> End_patt cpl0 (* this ensures precedence for overlapping patterns *) - | _ -> anomaly "tree is expected to end here" + | _ -> anomaly (Pp.str "tree is expected to end here") end | args::stack -> match args with @@ -959,7 +959,7 @@ let rec add_branch ((id,_) as cpl) pats tree= match tree with Close_patt t -> Close_patt (add_branch cpl stack t) - | _ -> anomaly "we should pop here" + | _ -> anomaly (Pp.str "we should pop here") end | (patt,rp) :: rest_args -> match patt with @@ -974,7 +974,7 @@ let rec add_branch ((id,_) as cpl) pats tree= (fun i bri -> append_branch cpl 1 (rest_args::stack) bri) tree - | _ -> anomaly "No pop/stop expected here" + | _ -> anomaly (Pp.str "No pop/stop expected here") end | PatCstr (_,(ind,cnum),args,nam) -> match tree with @@ -1002,7 +1002,7 @@ let rec add_branch ((id,_) as cpl) pats tree= (nargs::rest_args::stack) bri else bri in map_tree_rp rp (fun ids -> ids) mapi tree - | _ -> anomaly "No pop/stop expected here" + | _ -> anomaly (Pp.str "No pop/stop expected here") and append_branch ((id,_) as cpl) depth pats = function Some (ids,tree) -> Some (Id.Set.add id ids,append_tree cpl depth pats tree) @@ -1015,7 +1015,7 @@ and append_tree ((id,_) as cpl) depth pats tree = Close_patt (append_tree cpl (pred depth) pats t) | Skip_patt (ids,t) -> Skip_patt (Id.Set.add id ids,append_tree cpl depth pats t) - | End_patt _ -> anomaly "Premature end of branch" + | End_patt _ -> anomaly (Pp.str "Premature end of branch") | Split_patt (_,_,_) -> map_tree (Id.Set.add id) (fun i bri -> append_branch cpl (succ depth) pats bri) tree @@ -1105,7 +1105,7 @@ let case_tac params pat_info hyps gls0 = let et,per_info,ek,old_clauses,rest = match info.pm_stack with Per (et,pi,ek,old_clauses)::rest -> (et,pi,ek,old_clauses,rest) - | _ -> anomaly "wrong place for cases" in + | _ -> anomaly (Pp.str "wrong place for cases") in let clause = build_dep_clause params pat_info per_info hyps gls0 in let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in let nek = @@ -1130,7 +1130,7 @@ let initial_instance_stack ids : (_, _) instance_stack = List.map (fun id -> id,[None,[]]) ids let push_one_arg arg = function - [] -> anomaly "impossible" + [] -> anomaly (Pp.str "impossible") | (head,args) :: ctx -> ((head,(arg::args)) :: ctx) @@ -1148,7 +1148,7 @@ let push_head c ids stacks = let pop_one (id,stack) = let nstack= match stack with - [] -> anomaly "impossible" + [] -> anomaly (Pp.str "impossible") | [c] as l -> l | (Some head,args)::(head0,args0)::ctx -> let arg = applist (head,(List.rev args)) in @@ -1195,7 +1195,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = (applist (mkVar id, List.append param_metas (List.rev_append br_args hyp_metas)))) gls - | _ -> anomaly "wrong stack size" + | _ -> anomaly (Pp.str "wrong stack size") end | Split_patt (ids,ind,br), casee::next_objs -> let (mind,oind) as spec = Global.lookup_inductive ind in @@ -1262,11 +1262,11 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = (refine case_term) (Array.mapi branch_tac br) gls | Split_patt (_, _, _) , [] -> - anomaly "execute_cases : Nothing to split" + anomaly ~label:"execute_cases " (Pp.str "Nothing to split") | Skip_patt _ , [] -> - anomaly "execute_cases : Nothing to skip" + anomaly ~label:"execute_cases " (Pp.str "Nothing to skip") | End_patt (_,_) , _ :: _ -> - anomaly "execute_cases : End of branch with garbage left" + anomaly ~label:"execute_cases " (Pp.str "End of branch with garbage left") let understand_my_constr c gls = let env = pf_env gls in @@ -1289,14 +1289,14 @@ let end_tac et2 gls = let et1,pi,ek,clauses = match info.pm_stack with Suppose_case::_ -> - anomaly "This case should already be trapped" + anomaly (Pp.str "This case should already be trapped") | Claim::_ -> error "\"end claim\" expected." | Focus_claim::_ -> error "\"end focus\" expected." | Per(et',pi,ek,clauses)::_ -> (et',pi,ek,clauses) | [] -> - anomaly "This case should already be trapped" in + anomaly (Pp.str "This case should already be trapped") in let et = if et1 <> et2 then match et1 with @@ -1394,7 +1394,7 @@ let rec do_proof_instr_gen _thus _then instr = | Psuppose hyps -> suppose_tac hyps | Pcase (params,pat_info,hyps) -> case_tac params pat_info hyps | Pend (B_elim et) -> end_tac et - | Pend _ -> anomaly "Not applicable" + | Pend _ -> anomaly (Pp.str "Not applicable") | Pescape -> escape_tac let eval_instr {instr=instr} = @@ -1443,7 +1443,7 @@ let rec postprocess pts instr = with Type_errors.TypeError(env, Type_errors.IllFormedRecBody(_,_,_,_,_)) -> - anomaly "\"end induction\" generated an ill-formed fixpoint" + anomaly (Pp.str "\"end induction\" generated an ill-formed fixpoint") end | Pend _ -> goto_current_focus_or_top (pts) diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index c2b286f1b..0b7e94fa0 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -44,15 +44,15 @@ let pr_open_subgoals () = *) let pr_proof_instr instr = - Errors.anomaly "Cannot print a proof_instr" + Errors.anomaly (Pp.str "Cannot print a proof_instr") (* arnaud: Il nous faut quelque chose de type extr_genarg_printer si on veut aller dans cette direction Ppdecl_proof.pr_proof_instr (Global.env()) instr *) let pr_raw_proof_instr instr = - Errors.anomaly "Cannot print a raw proof_instr" + Errors.anomaly (Pp.str "Cannot print a raw proof_instr") let pr_glob_proof_instr instr = - Errors.anomaly "Cannot print a non-interpreted proof_instr" + Errors.anomaly (Pp.str "Cannot print a non-interpreted proof_instr") let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }= Decl_interp.interp_proof_instr diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml index 01f32e4a3..7f63c4200 100644 --- a/plugins/decl_mode/ppdecl_proof.ml +++ b/plugins/decl_mode/ppdecl_proof.ml @@ -75,7 +75,7 @@ and print_vars pconstr gtyp env sep _be _have vars = begin let nenv = match st.st_label with - Anonymous -> anomaly "anonymous variable" + Anonymous -> anomaly (Pp.str "anonymous variable") | Name id -> Environ.push_named (id,None,st.st_it) env in let pr_sep = if sep then pr_comma () else mt () in spc() ++ pr_sep ++ @@ -173,14 +173,14 @@ let rec pr_bare_proof_instr _then _thus env = function str "per" ++ spc () ++ pr_elim_type et ++ spc () ++ pr_casee env c | Pend (B_elim et) -> str "end" ++ spc () ++ pr_elim_type et - | _ -> anomaly "unprintable instruction" + | _ -> anomaly (Pp.str "unprintable instruction") let pr_emph = function 0 -> str " " | 1 -> str "* " | 2 -> str "** " | 3 -> str "*** " - | _ -> anomaly "unknown emphasis" + | _ -> anomaly (Pp.str "unknown emphasis") let pr_proof_instr env instr = pr_emph instr.emph ++ spc () ++ diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 7f5ad4f66..85b9bde71 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -348,7 +348,7 @@ and extract_seb env mp all = function | SEBstruct (msb) -> let env' = Modops.add_signature mp msb empty_delta_resolver env in MEstruct (mp,extract_sfb env' mp all msb) - | SEBwith (_,_) -> anomaly "Not available yet" + | SEBwith (_,_) -> anomaly (Pp.str "Not available yet") and extract_module env mp all mb = (* A module has an empty [mod_expr] when : diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 43a08657b..eb166675e 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -19,7 +19,7 @@ open Mlutil let rec msid_of_mt = function | MTident mp -> mp | MTwith(mt,_)-> msid_of_mt mt - | _ -> anomaly "Extraction:the With operator isn't applied to a name" + | _ -> anomaly ~label:"extraction" (Pp.str "the With operator isn't applied to a name") (*s Apply some functions upon all [ml_decl] and [ml_spec] found in a [ml_structure]. *) @@ -226,7 +226,7 @@ let get_decl_in_structure r struc = | _ -> error_not_visible r in go ll sel with Not_found -> - anomaly "reference not found in extracted structure" + anomaly (Pp.str "reference not found in extracted structure") (*s Optimization of a [ml_structure]. *) diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 74728f412..51946871f 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -242,7 +242,7 @@ let safe_basename_of_global r = let last_chance r = try Nametab.basename_of_global r with Not_found -> - anomaly "Inductive object unknown to extraction and not globally visible" + anomaly (Pp.str "Inductive object unknown to extraction and not globally visible") in match r with | ConstRef kn -> Label.to_id (con_label kn) diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index c7a582a0e..d39c6167b 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -75,7 +75,7 @@ let match_one_quantified_hyp setref seq lf= Left(Lforall(i,dom,triv))|Right(Rexists(i,dom,triv))-> if do_sequent setref triv lf.id seq i dom lf.atoms then setref:=IS.add ((Phantom dom),lf.id) !setref - | _ ->anomaly "can't happen" + | _ -> anomaly (Pp.str "can't happen") let give_instances lf seq= let setref=ref IS.empty in @@ -125,7 +125,7 @@ let mk_open_instance id gl m t= GLambda(loc,name,k,_,t0)-> let t1=raux (n-1) t0 in GLambda(loc,name,k,GHole (Loc.ghost,Evar_kinds.BinderType name),t1) - | _-> anomaly "can't happen" in + | _-> anomaly (Pp.str "can't happen") in let ntt=try Pretyping.understand evmap env (raux m rawt) with _ -> diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 7acabaaa4..c812deaf5 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -32,7 +32,7 @@ let wrap n b continue seq gls= let rec aux i nc ctx= if i<=0 then seq else match nc with - []->anomaly "Not the expected number of hyps" + []->anomaly (Pp.str "Not the expected number of hyps") | ((id,_,typ) as nd)::q-> if occur_var env id (pf_concl gls) || List.exists (occur_var_in_decl env id) ctx then diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 9c895e6a9..450b3ef40 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -310,7 +310,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = (fun i (end_of_type,ctxt_size,witness_fun) ((x',b',t') as decl) -> try let witness = Int.Map.find i sub in - if b' <> None then anomaly "can not redefine a rel!"; + if b' <> None then anomaly (Pp.str "can not redefine a rel!"); (Termops.pop end_of_type,ctxt_size,mkLetIn(x',witness,t',witness_fun)) with Not_found -> (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun) @@ -396,7 +396,7 @@ let rewrite_until_var arg_num eq_ids : tactic = then tclIDTAC g else match eq_ids with - | [] -> anomaly "Cannot find a way to prove recursive property"; + | [] -> anomaly (Pp.str "Cannot find a way to prove recursive property"); | eq_id::eq_ids -> tclTHEN (tclTRY (Equality.rewriteRL (mkVar eq_id))) @@ -604,7 +604,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = observe (str "cannot compute new term value : " ++ pr_gls g' ++ fnl () ++ str "last hyp is" ++ pr_lconstr_env (pf_env g') new_term_value_eq ); - anomaly "cannot compute new term value" + anomaly (Pp.str "cannot compute new term value") in let fun_body = mkLambda(Anonymous, @@ -830,7 +830,7 @@ let build_proof h_reduce_with_zeta Locusops.onConcl; build_proof do_finalize new_infos ] g - | Rel _ -> anomaly "Free var in goal conclusion !" + | Rel _ -> anomaly (Pp.str "Free var in goal conclusion !") and build_proof do_finalize dyn_infos g = (* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *) observe_tac_stream (str "build_proof with " ++ Printer.pr_lconstr dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g @@ -1014,7 +1014,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g = {finfos with equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with ConstRef c -> c - | _ -> Errors.anomaly "Not a constant" + | _ -> Errors.anomaly (Pp.str "Not a constant") ) } | _ -> () @@ -1208,7 +1208,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : else h_mutual_fix this_fix_info.name (this_fix_info.idx + 1) other_fix_infos - | _ -> anomaly "Not a valid information" + | _ -> anomaly (Pp.str "Not a valid information") in let first_tac : tactic = (* every operations until fix creations *) tclTHENSEQ @@ -1223,7 +1223,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : let ctxt,pte_app = (decompose_prod_assum (pf_concl gl)) in let pte,pte_args = (decompose_app pte_app) in try - let pte = try destVar pte with _ -> anomaly "Property is not a variable" in + let pte = try destVar pte with _ -> anomaly (Pp.str "Property is not a variable") in let fix_info = Id.Map.find pte ptes_to_fix in let nb_args = fix_info.nb_realargs in tclTHENSEQ @@ -1364,7 +1364,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : let prove_with_tcc tcc_lemma_constr eqs : tactic = match !tcc_lemma_constr with - | None -> anomaly "No tcc proof !!" + | None -> anomaly (Pp.str "No tcc proof !!") | Some lemma -> fun gls -> (* let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in *) @@ -1562,7 +1562,7 @@ let prove_principle_for_gen let args_ids = List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.args in let lemma = match !tcc_lemma_ref with - | None -> anomaly ( "No tcc proof !!") + | None -> anomaly (str "No tcc proof !!") | Some lemma -> lemma in (* let rec list_diff del_list check_list = *) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 700beaff5..9916ed95a 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -48,7 +48,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let id = Namegen.next_ident_away x avoid in Hashtbl.add tbl id x; (Name id,v,t)::(change_predicates_names (id::avoid) predicates) - | (Anonymous,_,_)::_ -> anomaly "Anonymous property binder " + | (Anonymous,_,_)::_ -> anomaly (Pp.str "Anonymous property binder ") in let avoid = (Termops.ids_of_context env_with_params ) in let princ_type_info = @@ -395,7 +395,7 @@ let get_funs_constant mp dp = let const = make_con mp dp (Label.of_id id) in const,i | Anonymous -> - anomaly "Anonymous fix" + anomaly (Pp.str "Anonymous fix") ) na | _ -> [|const,0|] @@ -505,7 +505,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis let first_type,other_princ_types = match l_schemes with s::l_schemes -> s,l_schemes - | _ -> anomaly "" + | _ -> anomaly (Pp.str "") in let (_,(const,_,_)) = try diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 8acd24c88..9ec935cfd 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1092,7 +1092,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) else GProd(Loc.ghost,n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude - | _ -> anomaly "Should not have an anonymous function here" + | _ -> anomaly (Pp.str "Should not have an anonymous function here") (* We have renamed all the anonymous functions during alpha_renaming phase *) end diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index a74ae84e2..868bf58c9 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -532,7 +532,7 @@ let rec are_unifiable_aux = function else let eqs' = try ((List.combine cpl1 cpl2)@eqs) - with _ -> anomaly "are_unifiable_aux" + with _ -> anomaly (Pp.str "are_unifiable_aux") in are_unifiable_aux eqs' @@ -554,7 +554,7 @@ let rec eq_cases_pattern_aux = function else let eqs' = try ((List.combine cpl1 cpl2)@eqs) - with _ -> anomaly "eq_cases_pattern_aux" + with _ -> anomaly (Pp.str "eq_cases_pattern_aux") in eq_cases_pattern_aux eqs' | _ -> raise NotUnifiable diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 6c3b009f8..850234c3b 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -641,7 +641,7 @@ let rec add_args id new_args b = CAppExpl(Loc.ghost,(None,r),new_args) | _ -> b end - | CFix _ | CCoFix _ -> anomaly "add_args : todo" + | CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo") | CProdN(loc,nal,b1) -> CProdN(loc, List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, @@ -692,10 +692,10 @@ let rec add_args id new_args b = CRecord (loc, (match w with Some w -> Some (add_args id new_args w) | _ -> None), List.map (fun (e,o) -> e, add_args id new_args o) pars) - | CNotation _ -> anomaly "add_args : CNotation" - | CGeneralization _ -> anomaly "add_args : CGeneralization" + | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation") + | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization") | CPrim _ -> b - | CDelimiters _ -> anomaly "add_args : CDelimiters" + | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters") exception Stop of Constrexpr.constr_expr @@ -736,7 +736,7 @@ let rec chop_n_arrow n t = chop_n_arrow new_n t' with Stop t -> t end - | _ -> anomaly "Not enough products" + | _ -> anomaly (Pp.str "Not enough products") let rec get_args b t : Constrexpr.local_binder list * diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index dfbfdce3a..a041205bf 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -389,7 +389,7 @@ let _ = let find_or_none id = try Some - (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> Errors.anomaly "Not a constant" + (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> Errors.anomaly (Pp.str "Not a constant") ) with Not_found -> None @@ -417,7 +417,7 @@ let add_Function is_general f = and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind") and graph_ind = match Nametab.locate (qualid_of_ident (mk_rel_id f_id)) - with | IndRef ind -> ind | _ -> Errors.anomaly "Not an inductive" + with | IndRef ind -> ind | _ -> Errors.anomaly (Pp.str "Not an inductive") in let finfos = { function_constant = f; diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index eed421159..a061cfaca 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -112,7 +112,7 @@ let generate_type g_to_f f graph i = let ctxt,_ = decompose_prod_assum graph_arity in let fun_ctxt,res_type = match ctxt with - | [] | [_] -> anomaly "Not a valid context" + | [] | [_] -> anomaly (Pp.str "Not a valid context") | (_,_,res_type)::fun_ctxt -> fun_ctxt,res_type in let rec args_from_decl i accu = function @@ -277,7 +277,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem (fun (_,pat) acc -> match pat with | Genarg.IntroIdentifier id -> Id.Set.add id acc - | _ -> anomaly "Not an identifier" + | _ -> anomaly (Pp.str "Not an identifier") ) (List.nth intro_pats (pred i)) Id.Set.empty @@ -316,7 +316,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem (fun (_,pat) acc -> match pat with | IntroIdentifier id -> id::acc - | _ -> anomaly "Not an identifier" + | _ -> anomaly (Pp.str "Not an identifier") ) (List.nth intro_pats (pred i)) [] @@ -423,7 +423,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem Array.map (fun (_,(ctxt,concl)) -> match ctxt with - | [] | [_] | [_;_] -> anomaly "bad context" + | [] | [_] | [_;_] -> anomaly (Pp.str "bad context") | hres::res::(x,_,t)::ctxt -> Termops.it_mkLambda_or_LetIn (Termops.it_mkProd_or_LetIn concl [hres;res]) @@ -488,7 +488,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem Array.map (fun (_,(ctxt,concl)) -> match ctxt with - | [] | [_] | [_;_] -> anomaly "bad context" + | [] | [_] | [_;_] -> anomaly (Pp.str "bad context") | hres::res::(x,_,t)::ctxt -> Termops.it_mkLambda_or_LetIn (Termops.it_mkProd_or_LetIn concl [hres;res]) @@ -541,7 +541,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem (fun (_,pat) acc -> match pat with | Genarg.IntroIdentifier id -> Id.Set.add id acc - | _ -> anomaly "Not an identifier" + | _ -> anomaly (Pp.str "Not an identifier") ) (List.nth intro_pats (pred i)) Id.Set.empty @@ -935,7 +935,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = then let eq_lemma = try Option.get (infos).equation_lemma - with Option.IsNone -> anomaly "Cannot find equation lemma" + with Option.IsNone -> anomaly (Pp.str "Cannot find equation lemma") in tclTHENSEQ[ tclMAP h_intro ids; @@ -1146,7 +1146,7 @@ let revert_graph kn post_tac hid g = let info = try find_Function_of_graph ind' with Not_found -> (* The graphs are mutually recursive but we cannot find one of them !*) - anomaly "Cannot retrieve infos about a mutual block" + anomaly (Pp.str "Cannot retrieve infos about a mutual block") in (* if we can find a completeness lemma for this function then we can come back to the functional form. If not, we do nothing diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 4b87a9b9c..8816d960f 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -73,8 +73,8 @@ let def_of_const t = | Some c -> Declarations.force c | _ -> assert false) with _ -> - anomaly ("Cannot find definition of constant "^ - (Id.to_string (Label.to_id (con_label sp)))) + anomaly (str "Cannot find definition of constant " ++ + (Id.print (Label.to_id (con_label sp)))) ) |_ -> assert false @@ -91,7 +91,7 @@ let constant sl s = (Id.of_string s)));; let const_of_ref = function ConstRef kn -> kn - | _ -> anomaly "ConstRef expected" + | _ -> anomaly (Pp.str "ConstRef expected") let nf_zeta env = @@ -426,7 +426,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) = travel jinfo new_continuation_tac {expr_info with info = b; is_final=false} end - | Rel _ -> anomaly "Free var in goal conclusion !" + | Rel _ -> anomaly (Pp.str "Free var in goal conclusion !") | Prod _ -> begin try @@ -1115,7 +1115,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a let f_id = match f_name with | Name f_id -> next_ident_away_in_goal f_id ids - | Anonymous -> anomaly "Anonymous function" + | Anonymous -> anomaly (Pp.str "Anonymous function") in let n_names_types,_ = decompose_lam_n nb_args body1 in let n_ids,ids = @@ -1125,7 +1125,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a | Name id -> let n_id = next_ident_away_in_goal id ids in n_id::n_ids,n_id::ids - | _ -> anomaly "anonymous argument" + | _ -> anomaly (Pp.str "anonymous argument") ) ([],(f_id::ids)) n_names_types @@ -1249,7 +1249,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ | Some s -> s | None -> try (add_suffix current_proof_name "_subproof") - with _ -> anomaly "open_new_goal with an unamed theorem" + with _ -> anomaly (Pp.str "open_new_goal with an unamed theorem") in let sign = initialize_named_context_for_proof () in let na = next_global_ident_away name [] in @@ -1261,7 +1261,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ let na_global = Nametab.global na_ref in match na_global with ConstRef c -> is_opaque_constant c - | _ -> anomaly "equation_lemma: not a constant" + | _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant") in let lemma = mkConst (Lib.make_con na) in ref_ := Some lemma ; @@ -1405,7 +1405,7 @@ let (com_eqn : int -> Id.t -> let opacity = match terminate_ref with | ConstRef c -> is_opaque_constant c - | _ -> anomaly "terminate_lemma: not a constant" + | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant") in let (evmap, env) = Lemmas.get_current_context() in let f_constr = constr_of_global f_ref in @@ -1499,7 +1499,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num begin if do_observe () then msg_debug (str "Cannot create equation Lemma " ++ Errors.print e) - else anomaly "Cannot create equation Lemma" + else anomaly (Pp.str "Cannot create equation Lemma") ; true end @@ -1533,7 +1533,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num with e -> begin (try ignore (Backtrack.backto previous_label) with _ -> ()); - (* anomaly "Cannot create termination Lemma" *) + (* anomaly (Pp.str "Cannot create termination Lemma") *) raise e end diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index eb713f251..a17c62eba 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -20,7 +20,7 @@ open Errors open Misctypes let out_arg = function - | ArgVar _ -> anomaly "Unevaluated or_var variable" + | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable") | ArgArg x -> x TACTIC EXTEND PsatzZ diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 851516945..c4961654d 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -318,7 +318,7 @@ let coq_iff = lazy (constant "iff") let evaluable_ref_of_constr s c = match kind_of_term (Lazy.force c) with | Const kn when Tacred.is_evaluable (Global.env()) (EvalConstRef kn) -> EvalConstRef kn - | _ -> anomaly ("Coq_omega: "^s^" is not an evaluable constant") + | _ -> anomaly ~label:"Coq_omega" (Pp.str (s^" is not an evaluable constant")) let sp_Zsucc = lazy (evaluable_ref_of_constr "Z.succ" coq_Zsucc) let sp_Zpred = lazy (evaluable_ref_of_constr "Z.pred" coq_Zpred) @@ -578,7 +578,7 @@ let compile name kind = let id = new_id () in tag_hypothesis name id; {kind = kind; body = List.rev accu; constant = n; id = id} - | _ -> anomaly "compile_equation" + | _ -> anomaly (Pp.str "compile_equation") in loop [] diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 4238037e7..2c41b95f3 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -410,7 +410,7 @@ let quote_terms ivs lc gl = | None -> begin match ivs.constant_lhs with | Some c_lhs -> Termops.subst_meta [1, c] c_lhs - | None -> anomaly "invalid inversion scheme for quote" + | None -> anomaly (Pp.str "invalid inversion scheme for quote") end | Some var_lhs -> begin match ivs.constant_lhs with diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 5cb97d4bd..1b9afb7c7 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -122,7 +122,7 @@ let add_step s sub = | SI_Or_r,[p] -> I_Or_r p | SE_Or i,[p1;p2] -> E_Or(i,p1,p2) | SD_Or i,[p] -> D_Or(i,p) - | _,_ -> anomaly "add_step: wrong arity" + | _,_ -> anomaly ~label:"add_step" (Pp.str "wrong arity") type 'a with_deps = {dep_it:'a; @@ -144,7 +144,7 @@ type state = let project = function Complete prf -> prf - | Incomplete (_,_) -> anomaly "not a successful state" + | Incomplete (_,_) -> anomaly (Pp.str "not a successful state") let pop n prf = let nprf= @@ -338,7 +338,7 @@ let search_norev seq= (Arrow(f2,f3))) f1; add_hyp (embed nseq) f3]):: !goals - | _ -> anomaly "search_no_rev: can't happen" in + | _ -> anomaly ~label:"search_no_rev" (Pp.str "can't happen") in Int.Map.iter add_one seq.norev_hyps; List.rev !goals @@ -363,7 +363,7 @@ let search_in_rev_hyps seq= | Arrow (Disjunct (f1,f2),f0) -> [make_step (SD_Or(i)), [add_hyp (add_hyp (embed nseq) (Arrow(f1,f0))) (Arrow (f2,f0))]] - | _ -> anomaly "search_in_rev_hyps: can't happen" + | _ -> anomaly ~label:"search_in_rev_hyps" (Pp.str "can't happen") with Not_found -> search_norev seq @@ -441,7 +441,7 @@ let branching = function | _::next -> s_info.nd_branching<-s_info.nd_branching+List.length next in List.map (append stack) successors - | Complete prf -> anomaly "already succeeded" + | Complete prf -> anomaly (Pp.str "already succeeded") open Pp diff --git a/plugins/xml/acic2Xml.ml4 b/plugins/xml/acic2Xml.ml4 index 34bb1d51f..9d3a10dba 100644 --- a/plugins/xml/acic2Xml.ml4 +++ b/plugins/xml/acic2Xml.ml4 @@ -21,7 +21,7 @@ let typesdtdname = "http://mowgli.cs.unibo.it/dtd/cictypes.dtd";; let rec find_last_id = function - [] -> Errors.anomaly "find_last_id: empty list" + [] -> Errors.anomaly ~label:"find_last_id" (Pp.str "empty list") | [id,_,_] -> id | _::tl -> find_last_id tl ;; diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index 4a8436d76..2772779d4 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -12,6 +12,8 @@ (* http://helm.cs.unibo.it *) (************************************************************************) +open Pp + (* Utility Functions *) exception TwoModulesWhoseDirPathIsOneAPrefixOfTheOther;; @@ -162,7 +164,7 @@ let family_of_term ty = match Term.kind_of_term ty with Term.Sort s -> Coq_sort (Term.family_of_sort s) | Term.Const _ -> CProp (* I could check that the constant is CProp *) - | _ -> Errors.anomaly "family_of_term" + | _ -> Errors.anomaly (Pp.str "family_of_term") ;; module CPropRetyping = @@ -177,7 +179,7 @@ module CPropRetyping = | h::rest -> match T.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma typ) with | T.Prod (na,c1,c2) -> subst_type env sigma (T.subst1 h c2) rest - | _ -> Errors.anomaly "Non-functional construction" + | _ -> Errors.anomaly (Pp.str "Non-functional construction") let sort_of_atomic_type env sigma ft args = @@ -193,7 +195,7 @@ let typeur sigma metamap = match Term.kind_of_term cstr with | T.Meta n -> (try T.strip_outer_cast (List.assoc n metamap) - with Not_found -> Errors.anomaly "type_of: this is not a well-typed term") + with Not_found -> Errors.anomaly ~label:"type_of" (Pp.str "this is not a well-typed term")) | T.Rel n -> let (_,_,ty) = Environ.lookup_rel n env in T.lift n ty @@ -202,7 +204,7 @@ let typeur sigma metamap = let (_,_,ty) = Environ.lookup_named id env in ty with Not_found -> - Errors.anomaly ("type_of: variable "^(Names.Id.to_string id)^" unbound")) + Errors.anomaly ~label:"type_of" (str "variable " ++ Names.Id.print id ++ str " unbound")) | T.Const c -> let cb = Environ.lookup_constant c env in Typeops.type_of_constant_type env (cb.Declarations.const_type) @@ -212,7 +214,7 @@ let typeur sigma metamap = | T.Case (_,p,c,lf) -> let Inductiveops.IndType(_,realargs) = try Inductiveops.find_rectype env sigma (type_of env c) - with Not_found -> Errors.anomaly "type_of: Bad recursive type" in + with Not_found -> Errors.anomaly ~label:"type_of" (Pp.str "Bad recursive type") in let t = Reductionops.whd_beta sigma (T.applist (p, realargs)) in (match Term.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma (type_of env t)) with | T.Prod _ -> Reductionops.whd_beta sigma (T.applist (t, [c])) @@ -253,7 +255,7 @@ let typeur sigma metamap = | _, (CProp as s) -> s) | T.App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args | T.Lambda _ | T.Fix _ | T.Construct _ -> - Errors.anomaly "sort_of: Not a type (1)" + Errors.anomaly ~label:"sort_of" (Pp.str "Not a type (1)") | _ -> outsort env sigma (type_of env t) and sort_family_of env t = @@ -265,7 +267,7 @@ let typeur sigma metamap = | T.App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args | T.Lambda _ | T.Fix _ | T.Construct _ -> - Errors.anomaly "sort_of: Not a type (1)" + Errors.anomaly ~label:"sort_of" (Pp.str "Not a type (1)") | _ -> outsort env sigma (type_of env t) in type_of, sort_of, sort_family_of @@ -514,7 +516,7 @@ print_endline "PASSATO" ; flush stdout ; add_inner_type fresh_id'' ; A.AEvar (fresh_id'', n, Array.to_list (Array.map (aux' env idrefs) l)) - | T.Meta _ -> Errors.anomaly "Meta met during exporting to XML" + | T.Meta _ -> Errors.anomaly (Pp.str "Meta met during exporting to XML") | T.Sort s -> A.ASort (fresh_id'', s) | T.Cast (v,_, t) -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index e16f9dd19..479b04228 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -289,7 +289,7 @@ let kind_of_variable id = | IsAssumption Conjectural -> "VARIABLE","Conjecture" | IsDefinition Definition -> "VARIABLE","LocalDefinition" | IsProof _ -> "VARIABLE","LocalFact" - | _ -> Errors.anomaly "Unsupported variable kind" + | _ -> Errors.anomaly (Pp.str "Unsupported variable kind") ;; let kind_of_constant kn = @@ -423,7 +423,7 @@ let print_ref qid fn = (* pretty prints via Xml.pp the proof in progress on dest *) let show_pftreestate internal fn (kind,pftst) id = if true then - Errors.anomaly "Xmlcommand.show_pftreestate is not supported in this version." + Errors.anomaly (Pp.str "Xmlcommand.show_pftreestate is not supported in this version.") let show fn = let pftst = Pfedit.get_pftreestate () in @@ -519,7 +519,7 @@ let _ = let options = " --html -s --body-only --no-index --latin1 --raw-comments" in let command cmd = if Sys.command cmd <> 0 then - Errors.anomaly ("Error executing \"" ^ cmd ^ "\"") + Errors.anomaly (Pp.str ("Error executing \"" ^ cmd ^ "\"")) in command (coqdoc^options^" -o "^fn^".xml "^fn^".v"); command ("rm "^fn^".v "^fn^".glob"); -- cgit v1.2.3