diff options
Diffstat (limited to 'plugins')
89 files changed, 173 insertions, 103 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index e3d27f719..7434f5e8a 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -9,6 +9,7 @@ (* This file implements the basic congruence-closure algorithm by *) (* Downey,Sethi and Tarjan. *) +open Errors open Util open Pp open Goptions diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index 78dbee3fe..d530495f8 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Term open Names diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index bb1d50c99..4c8c80ba4 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -9,6 +9,7 @@ (* This file uses the (non-compressed) union-find structure to generate *) (* proof-trees that will be transformed into proof-terms in cctac.ml4 *) +open Errors open Util open Names open Term diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index ec31f8917..0a3697e2a 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -26,6 +26,7 @@ open Ccalgo open Tacinterp open Ccproof open Pp +open Errors open Util open Format @@ -410,7 +411,7 @@ let cc_tactic depth additionnal_terms gls= begin str "\"congruence with (" ++ prlist_with_sep - (fun () -> str ")" ++ pr_spc () ++ str "(") + (fun () -> str ")" ++ spc () ++ str "(") (Termops.print_constr_env (pf_env gls)) terms_to_complete ++ str ")\"," diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli index fa6acaeb1..e84864f96 100644 --- a/plugins/decl_mode/decl_expr.mli +++ b/plugins/decl_mode/decl_expr.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Util +open Pp open Tacexpr type 'it statement = diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index b3e076c49..512269e55 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Topconstr diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index af6aa4bf5..5f9563cb2 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -9,6 +9,7 @@ open Names open Term open Evd +open Errors open Util diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index c1553b35d..e3a95fb4f 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Pp open Evd diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 27def8cc1..88e62e46d 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -46,15 +46,15 @@ let pr_open_subgoals () = *) let pr_proof_instr instr = - Util.anomaly "Cannot print a proof_instr" + Errors.anomaly "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 = - Util.anomaly "Cannot print a raw proof_instr" + Errors.anomaly "Cannot print a raw proof_instr" let pr_glob_proof_instr instr = - Util.anomaly "Cannot print a non-interpreted proof_instr" + Errors.anomaly "Cannot print a non-interpreted proof_instr" let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }= Decl_interp.interp_proof_instr @@ -65,7 +65,7 @@ let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }= let vernac_decl_proof () = let pf = Proof_global.give_me_the_proof () in if Proof.is_done pf then - Util.error "Nothing left to prove here." + Errors.error "Nothing left to prove here." else Proof.transaction pf begin fun () -> Decl_proof_instr.go_to_proof_mode () ; diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml index b866efaba..a2e078ee2 100644 --- a/plugins/decl_mode/ppdecl_proof.ml +++ b/plugins/decl_mode/ppdecl_proof.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Pp open Decl_expr diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml index 837195e44..fd96b6d1c 100644 --- a/plugins/dp/dp.ml +++ b/plugins/dp/dp.ml @@ -11,6 +11,7 @@ Zenon) *) +open Errors open Util open Pp open Libobject diff --git a/plugins/dp/dp_zenon.mll b/plugins/dp/dp_zenon.mll index 949e91e34..1e82034c0 100644 --- a/plugins/dp/dp_zenon.mll +++ b/plugins/dp/dp_zenon.mll @@ -3,7 +3,7 @@ open Lexing open Pp - open Util + open Errors open Names open Tacmach open Dp_why diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 0bd5b8434..1b443f753 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Term diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 73062328b..7c517dd9b 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -11,6 +11,7 @@ open Declarations open Names open Libnames open Pp +open Errors open Util open Miniml open Table diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 219b3913f..d9ee92c05 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -7,6 +7,7 @@ (************************************************************************) (*i*) +open Errors open Util open Names open Term diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 96731ed27..fe249cd65 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -9,6 +9,7 @@ (*s Production of Haskell syntax. *) open Pp +open Errors open Util open Names open Nameops diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index 5a19cc3f5..a5b57a474 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -9,6 +9,7 @@ (*s Target language for extraction: a core ML called MiniML. *) open Pp +open Errors open Util open Names open Libnames diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index c244e046d..f03170948 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -8,6 +8,7 @@ (*i*) open Pp +open Errors open Util open Names open Libnames diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index 029e8cf46..630db6f06 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Term diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 9e8dd8286..123edd4c3 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -10,6 +10,7 @@ open Names open Declarations open Environ open Libnames +open Errors open Util open Miniml open Table diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index ed69ec457..d99bca6f4 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -9,6 +9,7 @@ (*s Production of Ocaml syntax. *) open Pp +open Errors open Util open Names open Nameops diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index 215076555..157788ece 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -9,6 +9,7 @@ (*s Production of Scheme syntax. *) open Pp +open Errors open Util open Names open Nameops diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 238befd25..667182480 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -15,6 +15,7 @@ open Summary open Libobject open Goptions open Libnames +open Errors open Util open Pp open Miniml @@ -337,7 +338,7 @@ let warning_both_mod_and_cst q mp r = let error_axiom_scheme r i = err (str "The type scheme axiom " ++ spc () ++ - safe_pr_global r ++ spc () ++ str "needs " ++ pr_int i ++ + safe_pr_global r ++ spc () ++ str "needs " ++ int i ++ str " type variable(s).") let check_inside_module () = diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4 index 9e4f4d745..15c495ae7 100644 --- a/plugins/field/field.ml4 +++ b/plugins/field/field.ml4 @@ -15,6 +15,7 @@ open Tacinterp open Tacmach open Term open Typing +open Errors open Util open Vernacinterp open Vernacexpr diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index d67dceeac..566b2b8b0 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -12,6 +12,7 @@ open Term open Termops open Reductionops open Tacmach +open Errors open Util open Declarations open Libnames diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 4a38c48dc..f5b16e43f 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -17,7 +17,6 @@ open Tacticals open Tacinterp open Term open Names -open Util open Libnames (* declaring search depth as a global option *) @@ -103,6 +102,7 @@ let normalize_evaluables= unfold_in_hyp (Lazy.force defined_connectives) (Tacexpr.InHypType id)) *) +open Pp open Genarg open Ppconstr open Printer diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 16831d3ec..8d4b0eee1 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -10,6 +10,8 @@ open Formula open Sequent open Unify open Rules +open Pp +open Errors open Util open Term open Glob_term diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 23eeb2f66..b56fe4e50 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Term diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index f75678c60..780e3f3e7 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -7,6 +7,7 @@ (************************************************************************) open Term +open Errors open Util open Formula open Unify @@ -235,7 +236,7 @@ let print_cmap map= let print_entry c l s= let xc=Constrextern.extern_constr false (Global.env ()) c in str "| " ++ - Util.prlist Printer.pr_global l ++ + prlist Printer.pr_global l ++ str " : " ++ Ppconstr.pr_constr_expr xc ++ cut () ++ diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index c5c2bb954..5587e9fbb 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -7,6 +7,7 @@ (************************************************************************) open Term +open Errors open Util open Formula open Tacmach diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index 299a0054a..48c402cc0 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Formula open Tacmach diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 484937858..1a629aac9 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -503,11 +503,11 @@ let rec fourier gl= with _ -> ()) hyps; (* lineq = les inéquations découlant des hypothèses *) - if !lineq=[] then Util.error "No inequalities"; + if !lineq=[] then Errors.error "No inequalities"; let res=fourier_lineq (!lineq) in let tac=ref tclIDTAC in if res=[] - then Util.error "fourier failed" + then Errors.error "fourier failed" (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *) else (match res with [(cres,sres,lc)]-> diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 865074d6b..13b3dabdf 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1,4 +1,5 @@ open Printer +open Errors open Util open Term open Namegen @@ -1048,7 +1049,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 - | _ -> Util.anomaly "Not a constant" + | _ -> Errors.anomaly "Not a constant" ) } | _ -> () diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 6df9d574f..0f776ee6e 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -1,4 +1,5 @@ open Printer +open Errors open Util open Term open Namegen @@ -304,7 +305,7 @@ let defined () = Lemmas.save_named false with | UserError("extract_proof",msg) -> - Util.errorlabstrm + Errors.errorlabstrm "defined" ((try str "On goal : " ++ fnl () ++ pr_open_subgoals () ++ fnl () @@ -659,9 +660,9 @@ let build_scheme fas = try match Nametab.global f with | Libnames.ConstRef c -> c - | _ -> Util.error "Functional Scheme can only be used with functions" + | _ -> Errors.error "Functional Scheme can only be used with functions" with Not_found -> - Util.error ("Cannot find "^ Libnames.string_of_reference f) + Errors.error ("Cannot find "^ Libnames.string_of_reference f) in (f_as_constant,sort) ) @@ -692,7 +693,7 @@ let build_case_scheme fa = let funs = (fun (_,f,_) -> try Libnames.constr_of_global (Nametab.global f) with Not_found -> - Util.error ("Cannot find "^ Libnames.string_of_reference f)) fa in + Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in let first_fun = destConst funs in let funs_mp,funs_dp,_ = Names.repr_con first_fun in diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 123399d56..f330f9ff9 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -25,10 +25,10 @@ let pr_binding prc = function let pr_bindings prc prlc = function | Glob_term.ImplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ - Util.prlist_with_sep spc prc l + pr_sequence prc l | Glob_term.ExplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ - Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l + pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l | Glob_term.NoBindings -> mt () let pr_with_bindings prc prlc (c,bl) = @@ -111,7 +111,7 @@ TACTIC EXTEND snewfunind END -let pr_constr_coma_sequence prc _ _ = Util.prlist_with_sep Util.pr_comma prc +let pr_constr_coma_sequence prc _ _ = prlist_with_sep pr_comma prc ARGUMENT EXTEND constr_coma_sequence' TYPED AS constr_list @@ -180,12 +180,12 @@ let warning_error names e = | Building_graph e -> Pp.msg_warning (str "Cannot define graph(s) for " ++ - h 1 (prlist_with_sep (fun _ -> str","++spc ()) Libnames.pr_reference names) ++ + h 1 (pr_enum Libnames.pr_reference names) ++ if do_observe () then (spc () ++ Errors.print e) else mt ()) | Defining_principle e -> Pp.msg_warning (str "Cannot define principle(s) for "++ - h 1 (prlist_with_sep (fun _ -> str","++spc ()) Libnames.pr_reference names) ++ + h 1 (pr_enum Libnames.pr_reference names) ++ if do_observe () then Errors.print e else mt ()) | _ -> raise e @@ -207,7 +207,7 @@ VERNAC COMMAND EXTEND NewFunctionalScheme ; try Functional_principles_types.build_scheme fas with Functional_principles_types.No_graph_found -> - Util.error ("Cannot generate induction principle(s)") + Errors.error ("Cannot generate induction principle(s)") | e -> let names = List.map (fun (_,na,_) -> na) fas in warning_error names e @@ -377,7 +377,7 @@ let finduction (oid:identifier option) (heuristic: fapp_info list -> fapp_info l let info_list = find_fapp test g in let ordered_info_list = heuristic info_list in prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) ordered_info_list); - if List.length ordered_info_list = 0 then Util.error "function not found in goal\n"; + if List.length ordered_info_list = 0 then Errors.error "function not found in goal\n"; let taclist: Proof_type.tactic list = List.map (fun info -> @@ -419,7 +419,7 @@ TACTIC EXTEND finduction ["finduction" ident(id) natural_opt(oi)] -> [ match oi with - | Some(n) when n<=0 -> Util.error "numerical argument must be > 0" + | Some(n) when n<=0 -> Errors.error "numerical argument must be > 0" | _ -> let heuristic = chose_heuristic oi in finduction (Some id) heuristic tclIDTAC @@ -458,19 +458,19 @@ VERNAC COMMAND EXTEND MergeFunind "with" "(" ident(id2) ne_ident_list(cl2) ")" "using" ident(id) ] -> [ let f1 = Constrintern.interp_constr Evd.empty (Global.env()) - (CRef (Libnames.Ident (Util.dummy_loc,id1))) in + (CRef (Libnames.Ident (Pp.dummy_loc,id1))) in let f2 = Constrintern.interp_constr Evd.empty (Global.env()) - (CRef (Libnames.Ident (Util.dummy_loc,id2))) in + (CRef (Libnames.Ident (Pp.dummy_loc,id2))) in let f1type = Typing.type_of (Global.env()) Evd.empty f1 in let f2type = Typing.type_of (Global.env()) Evd.empty f2 in let ar1 = List.length (fst (decompose_prod f1type)) in let ar2 = List.length (fst (decompose_prod f2type)) in let _ = if ar1 <> List.length cl1 then - Util.error ("not the right number of arguments for " ^ string_of_id id1) in + Errors.error ("not the right number of arguments for " ^ string_of_id id1) in let _ = if ar2 <> List.length cl2 then - Util.error ("not the right number of arguments for " ^ string_of_id id2) in + Errors.error ("not the right number of arguments for " ^ string_of_id id2) in Merge.merge id1 id2 (Array.of_list cl1) (Array.of_list cl2) id ] END diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index c88c66693..6a5888874 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -5,6 +5,7 @@ open Term open Glob_term open Libnames open Indfun_common +open Errors open Util open Glob_termops @@ -977,8 +978,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = ((Util.list_chop nparam args')) in let rt_typ = - GApp(Util.dummy_loc, - GRef (Util.dummy_loc,Libnames.IndRef ind), + GApp(Pp.dummy_loc, + GRef (Pp.dummy_loc,Libnames.IndRef ind), (List.map (fun p -> Detyping.detype false [] (Termops.names_of_rel_context env) diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index cdd0eaf71..b458346d4 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -1,5 +1,6 @@ open Pp open Glob_term +open Errors open Util open Names (* Ocaml 3.06 Map.S does not handle is_empty *) diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index bfd153579..80a8811f1 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -84,9 +84,9 @@ val alpha_rt : Names.identifier list -> glob_constr -> glob_constr (* same as alpha_rt but for case branches *) val alpha_br : Names.identifier list -> - Util.loc * Names.identifier list * Glob_term.cases_pattern list * + Pp.loc * Names.identifier list * Glob_term.cases_pattern list * Glob_term.glob_constr -> - Util.loc * Names.identifier list * Glob_term.cases_pattern list * + Pp.loc * Names.identifier list * Glob_term.cases_pattern list * Glob_term.glob_constr diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 97a49d6f0..449dcd20e 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -1,3 +1,4 @@ +open Errors open Util open Names open Term diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index e65b58086..faa5f2e46 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -1,3 +1,4 @@ +open Errors open Util open Names open Term @@ -17,7 +18,7 @@ val functional_induction : bool -> Term.constr -> (Term.constr * Term.constr Glob_term.bindings) option -> - Genarg.intro_pattern_expr Util.located option -> + Genarg.intro_pattern_expr Pp.located option -> Proof_type.goal Tacmach.sigma -> Proof_type.goal list Evd.sigma diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index d6fb28ba5..60aa99b12 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -54,7 +54,7 @@ let locate_with_msg msg f x = try f x with - | Not_found -> raise (Util.UserError("", msg)) + | Not_found -> raise (Errors.UserError("", msg)) | e -> raise e @@ -79,7 +79,7 @@ let chop_rlambda_n = | Glob_term.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b | Glob_term.GLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b | _ -> - raise (Util.UserError("chop_rlambda_n", + raise (Errors.UserError("chop_rlambda_n", str "chop_rlambda_n: Not enough Lambdas")) in chop_lambda_n [] @@ -91,7 +91,7 @@ let chop_rprod_n = else match rt with | Glob_term.GProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b - | _ -> raise (Util.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products")) + | _ -> raise (Errors.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products")) in chop_prod_n [] @@ -112,10 +112,10 @@ let list_add_set_eq eq_fun x l = let const_of_id id = let _,princ_ref = - qualid_of_reference (Libnames.Ident (Util.dummy_loc,id)) + qualid_of_reference (Libnames.Ident (Pp.dummy_loc,id)) in try Nametab.locate_constant princ_ref - with Not_found -> Util.error ("cannot find "^ string_of_id id) + with Not_found -> Errors.error ("cannot find "^ string_of_id id) let def_of_const t = match (Term.kind_of_term t) with @@ -361,7 +361,7 @@ let pr_info f_info = let pr_table tb = let l = Cmap.fold (fun k v acc -> v::acc) tb [] in - Util.prlist_with_sep fnl pr_info l + Pp.prlist_with_sep fnl pr_info l let in_Function : function_info -> Libobject.obj = Libobject.declare_object @@ -397,7 +397,7 @@ let _ = let find_or_none id = try Some - (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> Util.anomaly "Not a constant" + (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> Errors.anomaly "Not a constant" ) with Not_found -> None @@ -425,7 +425,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 | _ -> Util.anomaly "Not an inductive" + with | IndRef ind -> ind | _ -> Errors.anomaly "Not an inductive" in let finfos = { function_constant = f; diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 9835ad605..a9b162819 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -7,6 +7,7 @@ (************************************************************************) open Tacexpr open Declarations +open Errors open Util open Names open Term @@ -29,10 +30,10 @@ let pr_binding prc = let pr_bindings prc prlc = function | Glob_term.ImplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ - Util.prlist_with_sep spc prc l + pr_sequence prc l | Glob_term.ExplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ - Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l + pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l | Glob_term.NoBindings -> mt () @@ -1142,7 +1143,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g mk_correct_id f_id in - ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,first_lemma_id) with _ -> ()); + ignore(try Vernacentries.vernac_reset_name (Pp.dummy_loc,first_lemma_id) with _ -> ()); raise e @@ -1239,7 +1240,7 @@ let invfun qhyp f = let f = match f with | ConstRef f -> f - | _ -> raise (Util.UserError("",str "Not a function")) + | _ -> raise (Errors.UserError("",str "Not a function")) in try let finfos = find_Function_infos f in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 4eedf8dc2..3b3f3057b 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -11,6 +11,7 @@ open Libnames open Tactics open Indfun_common +open Errors open Util open Topconstr open Vernacexpr diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 5e0aac4c2..c37de6e4a 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -17,6 +17,7 @@ open Pp open Names open Libnames open Nameops +open Errors open Util open Closure open RedFlags @@ -1273,7 +1274,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ let sign = initialize_named_context_for_proof () in let na = next_global_ident_away name [] in if Termops.occur_existential gls_type then - Util.error "\"abstract\" cannot handle existentials"; + Errors.error "\"abstract\" cannot handle existentials"; let hook _ _ = let opacity = let na_ref = Libnames.Ident (dummy_loc,na) in @@ -1553,7 +1554,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num hook with e -> begin - ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); + ignore(try Vernacentries.vernac_reset_name (Pp.dummy_loc,functional_id) with _ -> ()); (* anomaly "Cannot create termination Lemma" *) raise e end diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index 3b6b69879..9deeb6066 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -20,7 +20,7 @@ open Quote open Ring open Mutils open Glob_term -open Util +open Errors let out_arg = function | ArgVar _ -> anomaly "Unevaluated or_var variable" diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4 index a317307e0..c6d23afa6 100644 --- a/plugins/nsatz/nsatz.ml4 +++ b/plugins/nsatz/nsatz.ml4 @@ -9,6 +9,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) open Pp +open Errors open Util open Names open Term diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml index 45fcb2d25..b940ab89d 100644 --- a/plugins/nsatz/polynom.ml +++ b/plugins/nsatz/polynom.ml @@ -8,6 +8,7 @@ (* Recursive polynomials: R[x1]...[xn]. *) open Utile +open Errors open Util (* 1. Coefficients: R *) diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index d7dfe1491..1057c646f 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -13,6 +13,7 @@ (* *) (**************************************************************************) +open Errors open Util open Pp open Reduction diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index 84cc8464f..4aad8e738 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -25,7 +25,7 @@ let omega_tactic l = | "positive" -> Tacinterp.interp <:tactic<zify_positive>> | "N" -> Tacinterp.interp <:tactic<zify_N>> | "Z" -> Tacinterp.interp <:tactic<zify_op>> - | s -> Util.error ("No Omega knowledge base for type "^s)) + | s -> Errors.error ("No Omega knowledge base for type "^s)) (Util.list_uniquize (List.sort compare l)) in tclTHEN diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index 1f4ea97fd..4b3385677 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -open Util +open Pp open Tacexpr open Quote diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index fbb754204..fe025e6da 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -102,6 +102,7 @@ (*i*) open Pp +open Errors open Util open Names open Term diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml index 98d6361c0..b3151f26c 100644 --- a/plugins/ring/ring.ml +++ b/plugins/ring/ring.ml @@ -9,6 +9,7 @@ (* ML part of the Ring tactic *) open Pp +open Errors open Util open Flags open Term diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index e810e15c1..298b24850 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -39,7 +39,7 @@ let destructurate t = | Term.Var id,[] -> Kvar(Names.string_of_id id) | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body) | Term.Prod (Names.Name _,_,_),[] -> - Util.error "Omega: Not a quantifier-free goal" + Errors.error "Omega: Not a quantifier-free goal" | _ -> Kufo exception Destruct diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index 2db86e005..87e42354b 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -18,7 +18,7 @@ let romega_tactic l = | "positive" -> Tacinterp.interp <:tactic<zify_positive>> | "N" -> Tacinterp.interp <:tactic<zify_N>> | "Z" -> Tacinterp.interp <:tactic<zify_op>> - | s -> Util.error ("No ROmega knowledge base for type "^s)) + | s -> Errors.error ("No ROmega knowledge base for type "^s)) (Util.list_uniquize (List.sort compare l)) in tclTHEN diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 4a6d462ec..550a4af2b 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -6,6 +6,7 @@ *************************************************************************) +open Errors open Util open Const_omega module OmegaSolver = Omega.MakeOmegaSolver (Bigint) @@ -450,7 +451,7 @@ let rec scalar n = function | Omult(t1,Oint x) -> do_list [Lazy.force coq_c_mult_assoc_reduced], Omult(t1,Oint (n*x)) | Omult(t1,t2) -> - Util.error "Omega: Can't solve a goal with non-linear products" + Errors.error "Omega: Can't solve a goal with non-linear products" | (Oatom _ as t) -> do_list [], Omult(t,Oint n) | Oint i -> do_list [Lazy.force coq_c_reduce],Oint(n*i) | (Oufo _ as t)-> do_list [], Oufo (Omult(t,Oint n)) @@ -469,7 +470,7 @@ let rec negate = function | Omult(t1,Oint x) -> do_list [Lazy.force coq_c_opp_mult_r], Omult(t1,Oint (Bigint.neg x)) | Omult(t1,t2) -> - Util.error "Omega: Can't solve a goal with non-linear products" + Errors.error "Omega: Can't solve a goal with non-linear products" | (Oatom _ as t) -> do_list [Lazy.force coq_c_opp_one], Omult(t,Oint(negone)) | Oint i -> do_list [Lazy.force coq_c_reduce] ,Oint(Bigint.neg i) @@ -541,7 +542,7 @@ let shrink_pair f1 f2 = Lazy.force coq_c_red4, Omult(Oatom v,Oplus(c1,c2)) | t1,t2 -> oprint stdout t1; print_newline (); oprint stdout t2; print_newline (); - flush Pervasives.stdout; Util.error "shrink.1" + flush Pervasives.stdout; Errors.error "shrink.1" end (* \subsection{Calcul d'une sous formule constante} *) @@ -555,9 +556,9 @@ let reduce_factor = function let rec compute = function Oint n -> n | Oplus(t1,t2) -> compute t1 + compute t2 - | _ -> Util.error "condense.1" in + | _ -> Errors.error "condense.1" in [Lazy.force coq_c_reduce], Omult(Oatom v,Oint(compute c)) - | t -> Util.error "reduce_factor.1" + | t -> Errors.error "reduce_factor.1" (* \subsection{Réordonnancement} *) @@ -1291,7 +1292,7 @@ let total_reflexive_omega_tactic gl = let systems_list = destructurate_hyps full_reified_goal in if !debug then display_systems systems_list; resolution env full_reified_goal systems_list gl - with NO_CONTRADICTION -> Util.error "ROmega can't solve this system" + with NO_CONTRADICTION -> Errors.error "ROmega can't solve this system" (*i let tester = Tacmach.hide_atomic_tactic "TestOmega" test_tactic i*) diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index d773b1535..2448a2d39 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -7,6 +7,7 @@ (************************************************************************) open Term +open Errors open Util open Goptions diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 4a9a0e47f..60ef81286 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -8,6 +8,7 @@ module Search = Explore.Make(Proof_search) +open Errors open Util open Term open Names diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 9d61c06de..e834650ac 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -9,6 +9,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) open Pp +open Errors open Util open Names open Term diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml index f4d8b769c..0bde8dca9 100644 --- a/plugins/subtac/eterm.ml +++ b/plugins/subtac/eterm.ml @@ -11,6 +11,7 @@ open Names open Evd open List open Pp +open Errors open Util open Subtac_utils open Proof_type diff --git a/plugins/subtac/eterm.mli b/plugins/subtac/eterm.mli index 03d76f29a..4812fe0a6 100644 --- a/plugins/subtac/eterm.mli +++ b/plugins/subtac/eterm.mli @@ -11,6 +11,7 @@ open Tacmach open Term open Evd open Names +open Pp open Util open Tacinterp diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4 index c37f0db5a..27de89f67 100644 --- a/plugins/subtac/g_subtac.ml4 +++ b/plugins/subtac/g_subtac.ml4 @@ -14,7 +14,8 @@ open Flags -open Util +open Errors +open Pp open Names open Nameops open Vernacentries diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml index 710149ae4..cccb12e41 100644 --- a/plugins/subtac/subtac.ml +++ b/plugins/subtac/subtac.ml @@ -9,6 +9,7 @@ open Compat open Global open Pp +open Errors open Util open Names open Sign diff --git a/plugins/subtac/subtac.mli b/plugins/subtac/subtac.mli index b51150aa0..32d484091 100644 --- a/plugins/subtac/subtac.mli +++ b/plugins/subtac/subtac.mli @@ -1,2 +1,2 @@ val require_library : string -> unit -val subtac : Util.loc * Vernacexpr.vernac_expr -> unit +val subtac : Pp.loc * Vernacexpr.vernac_expr -> unit diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml index 16d4e21ee..d60841e72 100644 --- a/plugins/subtac/subtac_cases.ml +++ b/plugins/subtac/subtac_cases.ml @@ -7,6 +7,7 @@ (************************************************************************) open Cases +open Errors open Util open Names open Nameops diff --git a/plugins/subtac/subtac_cases.mli b/plugins/subtac/subtac_cases.mli index 77537d33a..11a811597 100644 --- a/plugins/subtac/subtac_cases.mli +++ b/plugins/subtac/subtac_cases.mli @@ -7,6 +7,7 @@ (************************************************************************) (*i*) +open Errors open Util open Names open Term diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml index cac0988c0..a81243f73 100644 --- a/plugins/subtac/subtac_classes.ml +++ b/plugins/subtac/subtac_classes.ml @@ -22,6 +22,7 @@ open Typeclasses open Typeclasses_errors open Decl_kinds open Entries +open Errors open Util module SPretyping = Subtac_pretyping.Pretyping @@ -71,8 +72,8 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p let t = if b then let _k = class_info cl in - CHole (Util.dummy_loc, Some Evd.InternalHole) - else CHole (Util.dummy_loc, None) + CHole (Pp.dummy_loc, Some Evd.InternalHole) + else CHole (Pp.dummy_loc, None) in t, avoid | None -> failwith ("new instance: under-applied typeclass")) cl @@ -149,7 +150,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p k.cl_projs; c :: props, rest' with Not_found -> - (CHole (Util.dummy_loc, None) :: props), rest + (CHole (Pp.dummy_loc, None) :: props), rest else props, rest) ([], props) k.cl_props in diff --git a/plugins/subtac/subtac_classes.mli b/plugins/subtac/subtac_classes.mli index 5b5c02037..5b8636a12 100644 --- a/plugins/subtac/subtac_classes.mli +++ b/plugins/subtac/subtac_classes.mli @@ -16,6 +16,7 @@ open Environ open Nametab open Mod_subst open Topconstr +open Errors open Util open Typeclasses open Implicit_quantifiers diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml index eb29bd045..3cbf9fcab 100644 --- a/plugins/subtac/subtac_coercion.ml +++ b/plugins/subtac/subtac_coercion.ml @@ -5,6 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Term diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml index ecae6759f..e5d93ace2 100644 --- a/plugins/subtac/subtac_command.ml +++ b/plugins/subtac/subtac_command.ml @@ -9,6 +9,7 @@ open Pp open Glob_term open Sign open Tacred +open Errors open Util open Names open Nameops diff --git a/plugins/subtac/subtac_errors.ml b/plugins/subtac/subtac_errors.ml index 067da150e..f07bbeb43 100644 --- a/plugins/subtac/subtac_errors.ml +++ b/plugins/subtac/subtac_errors.ml @@ -1,3 +1,4 @@ +open Errors open Util open Pp open Printer diff --git a/plugins/subtac/subtac_errors.mli b/plugins/subtac/subtac_errors.mli index 8d75b9c01..c65203075 100644 --- a/plugins/subtac/subtac_errors.mli +++ b/plugins/subtac/subtac_errors.mli @@ -1,13 +1,13 @@ type term_pp = Pp.std_ppcmds type subtyping_error = - UncoercibleInferType of Util.loc * term_pp * term_pp - | UncoercibleInferTerm of Util.loc * term_pp * term_pp * term_pp * term_pp + UncoercibleInferType of Pp.loc * term_pp * term_pp + | UncoercibleInferTerm of Pp.loc * term_pp * term_pp * term_pp * term_pp | UncoercibleRewrite of term_pp * term_pp type typing_error = - NonFunctionalApp of Util.loc * term_pp * term_pp * term_pp - | NonConvertible of Util.loc * term_pp * term_pp - | NonSigma of Util.loc * term_pp - | IllSorted of Util.loc * term_pp + NonFunctionalApp of Pp.loc * term_pp * term_pp * term_pp + | NonConvertible of Pp.loc * term_pp * term_pp + | NonSigma of Pp.loc * term_pp + | IllSorted of Pp.loc * term_pp exception Subtyping_error of subtyping_error exception Typing_error of typing_error exception Debug_msg of string diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index 6a5878b3e..527c5e084 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -11,6 +11,7 @@ open Summary open Libobject open Entries open Decl_kinds +open Errors open Util open Evd open Declare @@ -18,7 +19,7 @@ open Proof_type open Compat let ppwarn cmd = Pp.warn (str"Program:" ++ cmd) -let pperror cmd = Util.errorlabstrm "Program" cmd +let pperror cmd = Errors.errorlabstrm "Program" cmd let error s = pperror (str s) let reduce c = @@ -551,7 +552,7 @@ and solve_obligation_by_tac prg obls i tac = | Loc.Exc_located(_, Refiner.FailError (_, s)) | Refiner.FailError (_, s) -> user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s) - | Util.Anomaly _ as e -> raise e + | Errors.Anomaly _ as e -> raise e | e -> false and solve_prg_obligations prg ?oblset tac = diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli index c1d665aac..284e975db 100644 --- a/plugins/subtac/subtac_obligations.mli +++ b/plugins/subtac/subtac_obligations.mli @@ -1,4 +1,5 @@ open Names +open Pp open Util open Libnames open Evd diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml index 7c0d12325..c8acf7e0b 100644 --- a/plugins/subtac/subtac_pretyping.ml +++ b/plugins/subtac/subtac_pretyping.ml @@ -8,6 +8,7 @@ open Global open Pp +open Errors open Util open Names open Sign diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml index 528a2e683..fbeed381d 100644 --- a/plugins/subtac/subtac_pretyping_F.ml +++ b/plugins/subtac/subtac_pretyping_F.ml @@ -8,6 +8,7 @@ open Pp open Compat +open Errors open Util open Names open Sign diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml index 28bbdd35e..0ed78a23b 100644 --- a/plugins/subtac/subtac_utils.ml +++ b/plugins/subtac/subtac_utils.ml @@ -5,6 +5,8 @@ open Libnames open Coqlib open Term open Names +open Errors +open Pp open Util let ($) f x = f x @@ -426,7 +428,7 @@ let pr_meta_map evd = in prlist pr_meta_binding ml -let pr_idl idl = prlist_with_sep pr_spc pr_id idl +let pr_idl idl = pr_sequence pr_id idl let pr_evar_info evi = let phyps = @@ -443,14 +445,14 @@ let pr_evar_info evi = let pr_evar_map sigma = h 0 - (prlist_with_sep pr_fnl + (prlist_with_sep fnl (fun (ev,evi) -> h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi)) (to_list sigma)) let pr_constraints pbs = h 0 - (prlist_with_sep pr_fnl (fun (pbty,t1,t2) -> + (prlist_with_sep fnl (fun (pbty,t1,t2) -> Termops.print_constr t1 ++ spc() ++ str (match pbty with | Reduction.CONV -> "==" diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli index de96cc602..70ad0bcc8 100644 --- a/plugins/subtac/subtac_utils.mli +++ b/plugins/subtac/subtac_utils.mli @@ -7,6 +7,7 @@ open Evd open Decl_kinds open Topconstr open Glob_term +open Errors open Util open Evarutil open Names diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index bd2285bb3..cf51af134 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -7,6 +7,7 @@ (***********************************************************************) open Pp +open Errors open Util open Names open Pcoq diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index 446ae5225..5a355b971 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -11,6 +11,7 @@ (*i*) open Pcoq open Pp +open Errors open Util open Names open Coqlib @@ -20,6 +21,7 @@ open Bigint open Coqlib open Notation open Pp +open Errors open Util open Names (*i*) diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index 19a3c899f..cbc8d7fd6 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -111,7 +111,7 @@ let int31_of_pos_bigint dloc n = GApp (dloc, ref_construct, List.rev (args 31 n)) let error_negative dloc = - Util.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.") + Errors.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.") let interp_int31 dloc n = if is_pos_or_zero n then @@ -143,7 +143,7 @@ let uninterp_int31 i = let _ = Notation.declare_numeral_interpreter int31_scope (int31_path, int31_module) interp_int31 - ([GRef (Util.dummy_loc, int31_construct)], + ([GRef (Pp.dummy_loc, int31_construct)], uninterp_int31, true) @@ -201,7 +201,7 @@ let bigN_of_pos_bigint dloc n = result hght (word_of_pos_bigint dloc hght n) let bigN_error_negative dloc = - Util.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.") + Errors.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.") let interp_bigN dloc n = if is_pos_or_zero n then @@ -257,7 +257,7 @@ let uninterp_bigN rc = let bigN_list_of_constructors = let rec build i = if less_than i (add_1 n_inlined) then - GRef (Util.dummy_loc, bigN_constructor i)::(build (add_1 i)) + GRef (Pp.dummy_loc, bigN_constructor i)::(build (add_1 i)) else [] in @@ -303,8 +303,8 @@ let uninterp_bigZ rc = let _ = Notation.declare_numeral_interpreter bigZ_scope (bigZ_path, bigZ_module) interp_bigZ - ([GRef (Util.dummy_loc, bigZ_pos); - GRef (Util.dummy_loc, bigZ_neg)], + ([GRef (Pp.dummy_loc, bigZ_pos); + GRef (Pp.dummy_loc, bigZ_neg)], uninterp_bigZ, true) @@ -324,5 +324,5 @@ let uninterp_bigQ rc = let _ = Notation.declare_numeral_interpreter bigQ_scope (bigQ_path, bigQ_module) interp_bigQ - ([GRef (Util.dummy_loc, bigQ_z)], uninterp_bigQ, + ([GRef (Pp.dummy_loc, bigQ_z)], uninterp_bigQ, true) diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index b9c0bcd6f..b3195f281 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Pcoq diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index d670f6026..640806d87 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -7,6 +7,7 @@ (***********************************************************************) open Pp +open Errors open Util open Names open Pcoq diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index f8bce8f79..450d57969 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -8,6 +8,7 @@ open Pcoq open Pp +open Errors open Util open Names open Topconstr diff --git a/plugins/xml/acic2Xml.ml4 b/plugins/xml/acic2Xml.ml4 index 97f7e2bd4..75bc84074 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 - [] -> Util.anomaly "find_last_id: empty list" + [] -> Errors.anomaly "find_last_id: empty list" | [id,_,_] -> id | _::tl -> find_last_id tl ;; diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index da0a65ff5..78a402898 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -59,7 +59,7 @@ let get_uri_of_var v pvars = let module N = Names in let rec search_in_open_sections = function - [] -> Util.error ("Variable "^v^" not found") + [] -> Errors.error ("Variable "^v^" not found") | he::tl as modules -> let dirpath = N.make_dirpath modules in if List.mem (N.id_of_string v) (D.last_section_hyps dirpath) then @@ -162,7 +162,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 *) - | _ -> Util.anomaly "family_of_term" + | _ -> Errors.anomaly "family_of_term" ;; module CPropRetyping = @@ -177,7 +177,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 - | _ -> Util.anomaly "Non-functional construction" + | _ -> Errors.anomaly "Non-functional construction" let sort_of_atomic_type env sigma ft args = @@ -193,7 +193,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 -> Util.anomaly "type_of: this is not a well-typed term") + with Not_found -> Errors.anomaly "type_of: this is not a well-typed term") | T.Rel n -> let (_,_,ty) = Environ.lookup_rel n env in T.lift n ty @@ -202,7 +202,7 @@ let typeur sigma metamap = let (_,_,ty) = Environ.lookup_named id env in ty with Not_found -> - Util.anomaly ("type_of: variable "^(Names.string_of_id id)^" unbound")) + Errors.anomaly ("type_of: variable "^(Names.string_of_id id)^" unbound")) | T.Const c -> let cb = Environ.lookup_constant c env in Typeops.type_of_constant_type env (cb.Declarations.const_type) @@ -212,7 +212,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 -> Util.anomaly "type_of: Bad recursive type" in + with Not_found -> Errors.anomaly "type_of: 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 +253,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 _ -> - Util.anomaly "sort_of: Not a type (1)" + Errors.anomaly "sort_of: Not a type (1)" | _ -> outsort env sigma (type_of env t) and sort_family_of env t = @@ -265,7 +265,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 _ -> - Util.anomaly "sort_of: Not a type (1)" + Errors.anomaly "sort_of: Not a type (1)" | _ -> outsort env sigma (type_of env t) in type_of, sort_of, sort_family_of @@ -523,7 +523,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 _ -> Util.anomaly "Meta met during exporting to XML" + | T.Meta _ -> Errors.anomaly "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 ; @@ -737,7 +737,7 @@ print_endline "PASSATO" ; flush stdout ; let ids = ref (Termops.ids_of_context env) in Array.map (function - N.Anonymous -> Util.error "Anonymous fix function met" + N.Anonymous -> Errors.error "Anonymous fix function met" | N.Name id as n -> let res = N.Name (Namegen.next_name_away n !ids) in ids := id::!ids ; @@ -750,7 +750,7 @@ print_endline "PASSATO" ; flush stdout ; let fi' = match fi with N.Name fi -> fi - | N.Anonymous -> Util.error "Anonymous fix function met" + | N.Anonymous -> Errors.error "Anonymous fix function met" in (id, fi', ai, aux' env idrefs ti, @@ -771,7 +771,7 @@ print_endline "PASSATO" ; flush stdout ; let ids = ref (Termops.ids_of_context env) in Array.map (function - N.Anonymous -> Util.error "Anonymous fix function met" + N.Anonymous -> Errors.error "Anonymous fix function met" | N.Name id as n -> let res = N.Name (Namegen.next_name_away n !ids) in ids := id::!ids ; @@ -784,7 +784,7 @@ print_endline "PASSATO" ; flush stdout ; let fi' = match fi with N.Name fi -> fi - | N.Anonymous -> Util.error "Anonymous fix function met" + | N.Anonymous -> Errors.error "Anonymous fix function met" in (id, fi', aux' env idrefs ti, diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml index a21a919ad..30cd5c18b 100644 --- a/plugins/xml/doubleTypeInference.ml +++ b/plugins/xml/doubleTypeInference.ml @@ -67,7 +67,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types = let judgement = match T.kind_of_term cstr with T.Meta n -> - Util.error + Errors.error "DoubleTypeInference.double_type_of: found a non-instanciated goal" | T.Evar ((n,l) as ev) -> diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4 index 3c3e54fa3..69b9e6ea7 100644 --- a/plugins/xml/dumptree.ml4 +++ b/plugins/xml/dumptree.ml4 @@ -128,7 +128,7 @@ let pr_goal_xml sigma g = ;; let print_proof_xml () = - Util.anomaly "Dump Tree command not supported in this version." + Errors.anomaly "Dump Tree command not supported in this version." VERNAC COMMAND EXTEND DumpTree diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4 index 2f5eb6ac2..21058a7b9 100644 --- a/plugins/xml/proofTree2Xml.ml4 +++ b/plugins/xml/proofTree2Xml.ml4 @@ -53,7 +53,7 @@ let constr_to_xml obj sigma env = in Acic2Xml.print_term ids_to_inner_sorts annobj with e -> - Util.anomaly + Errors.anomaly ("Problem during the conversion of constr into XML: " ^ Printexc.to_string e) (* CSC: debugging stuff diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 1037bbf08..13821488a 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -424,7 +424,7 @@ let kind_of_variable id = | DK.IsAssumption DK.Conjectural -> "VARIABLE","Conjecture" | DK.IsDefinition DK.Definition -> "VARIABLE","LocalDefinition" | DK.IsProof _ -> "VARIABLE","LocalFact" - | _ -> Util.anomaly "Unsupported variable kind" + | _ -> Errors.anomaly "Unsupported variable kind" ;; let kind_of_constant kn = @@ -541,7 +541,7 @@ let print internal glob_ref kind xml_library_root = D.mind_finite=finite} = mib in Cic2acic.Inductive kn,mk_inductive_obj kn mib packs variables nparams hyps finite | Ln.ConstructRef _ -> - Util.error ("a single constructor cannot be printed in XML") + Errors.error ("a single constructor cannot be printed in XML") in let fn = filename_of_path xml_library_root tag in let uri = Cic2acic.uri_of_kernel_name tag in @@ -560,7 +560,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 - Util.anomaly "Xmlcommand.show_pftreestate is not supported in this version." + Errors.anomaly "Xmlcommand.show_pftreestate is not supported in this version." let show fn = let pftst = Pfedit.get_pftreestate () in @@ -656,7 +656,7 @@ let _ = let options = " --html -s --body-only --no-index --latin1 --raw-comments" in let command cmd = if Sys.command cmd <> 0 then - Util.anomaly ("Error executing \"" ^ cmd ^ "\"") + Errors.anomaly ("Error executing \"" ^ cmd ^ "\"") in command (coqdoc^options^" -o "^fn^".xml "^fn^".v"); command ("rm "^fn^".v "^fn^".glob"); |