From fc579fdc83b751a44a18d2373e86ab38806e7306 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 19 Aug 2016 02:35:47 +0200 Subject: Make the user_err header an optional parameter. Suggested by @ppedrot --- proofs/clenv.ml | 22 +++++++++++----------- proofs/evar_refiner.ml | 2 +- proofs/logic.ml | 14 +++++++------- proofs/pfedit.ml | 4 ++-- proofs/proof.ml | 4 ++-- proofs/proof_global.ml | 6 +++--- proofs/redexpr.ml | 10 +++++----- proofs/refiner.ml | 12 ++++++------ 8 files changed, 37 insertions(+), 37 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 0ee13bb63..fad656223 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -155,7 +155,7 @@ let error_incompatible_inst clenv mv = let na = meta_name clenv.evd mv in match na with Name id -> - user_err "clenv_assign" + user_err ~hdr:"clenv_assign" (str "An incompatible instantiation has already been found for " ++ pr_id id) | _ -> @@ -417,11 +417,11 @@ let qhyp_eq h1 h2 = match h1, h2 with let check_bindings bl = match List.duplicates qhyp_eq (List.map pi2 bl) with | NamedHyp s :: _ -> - user_err "" + user_err (str "The variable " ++ pr_id s ++ str " occurs more than once in binding list."); | AnonHyp n :: _ -> - user_err "" + user_err (str "The position " ++ int n ++ str " occurs more than once in binding list.") | [] -> () @@ -435,7 +435,7 @@ let explain_no_such_bound_variable evd id = if na != Anonymous then out_name na :: l else l in let mvl = List.fold_left fold [] (Evd.meta_list evd) in - user_err "Evd.meta_with_name" + user_err ~hdr:"Evd.meta_with_name" (str"No such bound variable " ++ pr_id id ++ (if mvl == [] then str " (no bound variables at all in the expression)." else @@ -460,7 +460,7 @@ let meta_with_name evd id = | ([n],_|_,[n]) -> n | _ -> - user_err "Evd.meta_with_name" + user_err ~hdr:"Evd.meta_with_name" (str "Binder name \"" ++ pr_id id ++ strbrk "\" occurs more than once in clause.") @@ -469,12 +469,12 @@ let meta_of_binder clause loc mvs = function | AnonHyp n -> try List.nth mvs (n-1) with (Failure _|Invalid_argument _) -> - user_err "" (str "No such binder.") + user_err (str "No such binder.") let error_already_defined b = match b with | NamedHyp id -> - user_err "" + user_err (str "Binder name \"" ++ pr_id id ++ str"\" already defined with incompatible value.") | AnonHyp n -> @@ -527,7 +527,7 @@ let clenv_constrain_last_binding c clenv = clenv_assign_binding clenv k c let error_not_right_number_missing_arguments n = - user_err "" + user_err (strbrk "Not the right number of missing arguments (expected " ++ int n ++ str ").") @@ -641,7 +641,7 @@ let explain_no_such_bound_variable holes id = | [id] -> str "(possible name is: " ++ pr_id id ++ str ")." | _ -> str "(possible names are: " ++ pr_enum pr_id mvl ++ str ")." in - user_err "" (str "No such bound variable " ++ pr_id id ++ expl) + user_err (str "No such bound variable " ++ pr_id id ++ expl) let evar_with_name holes id = let map h = match h.hole_name with @@ -653,7 +653,7 @@ let evar_with_name holes id = | [] -> explain_no_such_bound_variable holes id | [h] -> h.hole_evar | _ -> - user_err "" + user_err (str "Binder name \"" ++ pr_id id ++ str "\" occurs more than once in clause.") @@ -664,7 +664,7 @@ let evar_of_binder holes = function let h = List.nth holes (pred n) in h.hole_evar with e when CErrors.noncritical e -> - user_err "" (str "No such binder.") + user_err (str "No such binder.") let define_with_type sigma env ev c = let t = Retyping.get_type_of env sigma ev in diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index ce216e563..ff0df9179 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -54,7 +54,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc with e when CErrors.noncritical e -> let loc = Glob_ops.loc_of_glob_constr rawc in - user_err ~loc "" + user_err ~loc (str "Instance is not well-typed in the environment of " ++ pr_existential_key sigma evk ++ str ".") in diff --git a/proofs/logic.ml b/proofs/logic.ml index 9f34f5cf6..3e77bef7e 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -151,7 +151,7 @@ let reorder_context env sign ord = | top::ord' when mem_q top moved_hyps -> let ((d,h),mh) = find_q top moved_hyps in if occur_vars_in_decl env h d then - user_err "reorder_context" + user_err ~hdr:"reorder_context" (str "Cannot move declaration " ++ pr_id top ++ spc() ++ str "before " ++ pr_sequence pr_id @@ -182,7 +182,7 @@ let check_decl_position env sign d = let needed = global_vars_set_of_decl env d in let deps = dependency_closure env (named_context_of_val sign) needed in if Id.List.mem x deps then - user_err "Logic.check_decl_position" + user_err ~hdr:"Logic.check_decl_position" (str "Cannot create self-referring hypothesis " ++ pr_id x); x::deps @@ -252,7 +252,7 @@ let move_hyp toleft (left,declfrom,right) hto = if not (move_location_eq hto (MoveAfter hyp)) then (first, d::middle) else - user_err "move_hyp" (str "Cannot move " ++ pr_id (get_id declfrom) ++ + user_err ~hdr:"move_hyp" (str "Cannot move " ++ pr_id (get_id declfrom) ++ Miscprint.pr_move_location pr_id hto ++ str (if toleft then ": it occurs in " else ": it depends on ") ++ pr_id hyp ++ str ".") @@ -287,7 +287,7 @@ let move_hyp toleft (left,declfrom,right) hto = variables only in Application and Case *) let error_unsupported_deep_meta c = - user_err "" (strbrk "Application of lemmas whose beta-iota normal " ++ + user_err (strbrk "Application of lemmas whose beta-iota normal " ++ strbrk "form contains metavariables deep inside the term is not " ++ strbrk "supported; try \"refine\" instead.") @@ -498,10 +498,10 @@ let convert_hyp check sign sigma d = let _,c,ct = to_tuple d' in let env = Global.env_of_context sign in if check && not (is_conv env sigma bt ct) then - user_err "Logic.convert_hyp" + user_err ~hdr:"Logic.convert_hyp" (str "Incorrect change of the type of " ++ pr_id id ++ str "."); if check && not (Option.equal (is_conv env sigma) b c) then - user_err "Logic.convert_hyp" + user_err ~hdr:"Logic.convert_hyp" (str "Incorrect change of the body of "++ pr_id id ++ str "."); if check then reorder := check_decl_position env sign d; d) in @@ -534,7 +534,7 @@ let prim_refiner r sigma goal = t,cl,sigma else (if !check && mem_named_context id (named_context_of_val sign) then - user_err "Logic.prim_refiner" + user_err ~hdr:"Logic.prim_refiner" (str "Variable " ++ pr_id id ++ str " is already declared."); push_named_context_val (LocalAssum (id,t)) sign,t,cl,sigma) in let (sg2,ev2,sigma) = diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index b86582def..86c2b7a57 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -131,7 +131,7 @@ let solve ?with_end_tac gi info_lvl tac pr = | CList.IndexOutOfRange -> match gi with | Vernacexpr.SelectNth i -> let msg = str "No such goal: " ++ int i ++ str "." in - CErrors.user_err "" msg + CErrors.user_err msg | _ -> assert false let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac) @@ -228,7 +228,7 @@ let solve_by_implicit_tactic env sigma evk = when Context.Named.equal (Environ.named_context_of_val evi.evar_hyps) (Environ.named_context env) -> - let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError ("",Pp.str"Proof is not complete."))) []) in + let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError (None,Pp.str"Proof is not complete."))) []) in (try let c = Evarutil.nf_evars_universes sigma evi.evar_concl in if Evarutil.has_undefined_evars sigma c then raise Exit; diff --git a/proofs/proof.ml b/proofs/proof.ml index 2e5330b4b..16278b456 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -68,9 +68,9 @@ let _ = CErrors.register_handler begin function | CannotUnfocusThisWay -> CErrors.error "This proof is focused, but cannot be unfocused this way" | NoSuchGoals (i,j) when Int.equal i j -> - CErrors.user_err "Focus" Pp.(str"No such goal (" ++ int i ++ str").") + CErrors.user_err ~hdr:"Focus" Pp.(str"No such goal (" ++ int i ++ str").") | NoSuchGoals (i,j) -> - CErrors.user_err "Focus" Pp.( + CErrors.user_err ~hdr:"Focus" Pp.( str"Not every goal in range ["++ int i ++ str","++int j++str"] exist." ) | FullyUnfocused -> CErrors.error "The proof is not focused" diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 107a3a7e5..da0af3c62 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -203,7 +203,7 @@ let discard (loc,id) = discard_gen id; if Int.equal (List.length !pstates) n then CErrors.user_err ~loc - "Pfedit.delete_proof" (str"No such proof" ++ msg_proofs ()) + ~hdr:"Pfedit.delete_proof" (str"No such proof" ++ msg_proofs ()) let discard_current () = if List.is_empty !pstates then raise NoCurrentProof else pstates := List.tl !pstates @@ -408,7 +408,7 @@ let return_proof ?(allow_partial=false) () = let evd = let error s = let prf = str " (in proof " ++ Id.print pid ++ str ")" in - raise (CErrors.UserError("last tactic before Qed",s ++ prf)) + raise (CErrors.UserError(Some "last tactic before Qed",s ++ prf)) in try Proof.return proof with | Proof.UnfinishedProof -> @@ -519,7 +519,7 @@ module Bullet = struct (function | FailedBullet (b,sugg) -> let prefix = str"Wrong bullet " ++ pr_bullet b ++ str" : " in - CErrors.user_err "Focus" (prefix ++ suggest_on_error sugg) + CErrors.user_err ~hdr:"Focus" (prefix ++ suggest_on_error sugg) | _ -> raise CErrors.Unhandled) diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index cafd46849..41ad7d94e 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -73,7 +73,7 @@ let set_strategy_one ref l = let cb = Global.lookup_constant sp in (match cb.const_body with | OpaqueDef _ -> - user_err "set_transparent_const" + user_err ~hdr:"set_transparent_const" (str "Cannot make" ++ spc () ++ Nametab.pr_global_env Id.Set.empty (ConstRef sp) ++ spc () ++ str "transparent because it was declared opaque."); @@ -175,19 +175,19 @@ let red_expr_tab = Summary.ref String.Map.empty ~name:"Declare Reduction" let declare_reduction s f = if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab - then user_err "Redexpr.declare_reduction" + then user_err ~hdr:"Redexpr.declare_reduction" (str "There is already a reduction expression of name " ++ str s) else reduction_tab := String.Map.add s f !reduction_tab let check_custom = function | ExtraRedExpr s -> if not (String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab) - then user_err "Redexpr.check_custom" (str "Reference to undefined reduction expression " ++ str s) + then user_err ~hdr:"Redexpr.check_custom" (str "Reference to undefined reduction expression " ++ str s) |_ -> () let decl_red_expr s e = if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab - then user_err "Redexpr.decl_red_expr" + then user_err ~hdr:"Redexpr.decl_red_expr" (str "There is already a reduction expression of name " ++ str s) else begin check_custom e; @@ -247,7 +247,7 @@ let reduction_of_red_expr env = with Not_found -> (try reduction_of_red_expr (String.Map.find s !red_expr_tab) with Not_found -> - user_err "Redexpr.reduction_of_red_expr" + user_err ~hdr:"Redexpr.reduction_of_red_expr" (str "unknown user-defined reduction \"" ++ str s ++ str "\""))) | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast) | CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 65a889882..3e59631b7 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -60,7 +60,7 @@ let tclIDTAC_MESSAGE s gls = Feedback.msg_info (hov 0 s); tclIDTAC gls (* General failure tactic *) -let tclFAIL_s s gls = user_err "Refiner.tclFAIL_s" (str s) +let tclFAIL_s s gls = user_err ~hdr:"Refiner.tclFAIL_s" (str s) (* A special exception for levels for the Fail tactic *) exception FailError of int * std_ppcmds Lazy.t @@ -82,7 +82,7 @@ let thens3parts_tac tacfi tac tacli (sigr,gs) = let nf = Array.length tacfi in let nl = Array.length tacli in let ng = List.length gs in - if ng apply_sig_tac sigr (if i=ng-nl then tacli.(nl-ng+i) else tac)) @@ -164,14 +164,14 @@ the goal unchanged *) let tclWEAK_PROGRESS tac ptree = let rslt = tac ptree in if Goal.V82.weak_progress rslt ptree then rslt - else user_err "Refiner.WEAK_PROGRESS" (str"Failed to progress.") + else user_err ~hdr:"Refiner.WEAK_PROGRESS" (str"Failed to progress.") (* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves the goal unchanged *) let tclPROGRESS tac ptree = let rslt = tac ptree in if Goal.V82.progress rslt ptree then rslt - else user_err "Refiner.PROGRESS" (str"Failed to progress.") + else user_err ~hdr:"Refiner.PROGRESS" (str"Failed to progress.") (* Same as tclWEAK_PROGRESS but fails also if tactics generates several goals, one of them being identical to the original goal *) @@ -182,7 +182,7 @@ let tclNOTSAMEGOAL (tac : tactic) goal = let rslt = tac goal in let {it=gls;sigma=sigma} = rslt in if List.exists (same_goal goal sigma) gls - then user_err "Refiner.tclNOTSAMEGOAL" + then user_err ~hdr:"Refiner.tclNOTSAMEGOAL" (str"Tactic generated a subgoal identical to the original goal.") else rslt @@ -316,7 +316,7 @@ let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl) let tclDO n t = let rec dorec k = - if k < 0 then user_err "Refiner.tclDO" + if k < 0 then user_err ~hdr:"Refiner.tclDO" (str"Wrong argument : Do needs a positive integer."); if Int.equal k 0 then tclIDTAC else if Int.equal k 1 then t else (tclTHEN t (dorec (k-1))) -- cgit v1.2.3