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 --- plugins/cc/cctac.ml | 2 +- plugins/decl_mode/decl_interp.ml | 6 +++--- plugins/decl_mode/decl_proof_instr.ml | 6 +++--- plugins/extraction/table.ml | 2 +- plugins/funind/functional_principles_types.ml | 4 ++-- plugins/funind/glob_term_to_relation.ml | 6 +++--- plugins/funind/glob_termops.ml | 6 +++--- plugins/funind/indfun.ml | 20 ++++++++++---------- plugins/funind/indfun_common.ml | 8 ++++---- plugins/funind/invfun.ml | 10 +++++----- plugins/funind/merge.ml | 2 +- plugins/funind/recdef.ml | 14 +++++++------- plugins/rtauto/refl_tauto.ml | 4 ++-- plugins/setoid_ring/newring.ml | 10 +++++----- plugins/ssrmatching/ssrmatching.ml4 | 4 ++-- plugins/syntax/ascii_syntax.ml | 2 +- plugins/syntax/nat_syntax.ml | 2 +- plugins/syntax/numbers_syntax.ml | 4 ++-- plugins/syntax/z_syntax.ml | 4 ++-- 19 files changed, 58 insertions(+), 58 deletions(-) (limited to 'plugins') diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 6ed678176..71e2180a5 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -456,7 +456,7 @@ let cc_tactic depth additionnal_terms = end } let cc_fail gls = - user_err "Congruence" (Pp.str "congruence failed.") + user_err ~hdr:"Congruence" (Pp.str "congruence failed.") let congruence_tac depth l = Tacticals.New.tclORELSE diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 9ed5c61e2..f68c01b18 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -91,7 +91,7 @@ let rec add_vars_of_simple_pattern globs = function (UserError ("simple_pattern",str "\"as\" is not allowed here"))*) | CPatOr (loc, _)-> Loc.raise ~loc - (UserError ("simple_pattern",str "\"(_ | _)\" is not allowed here")) + (UserError (Some "simple_pattern",str "\"(_ | _)\" is not allowed here")) | CPatDelimiters (_,_,p) -> add_vars_of_simple_pattern globs p | CPatCstr (_,_,pl1,pl2) -> @@ -328,7 +328,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps = let _ = let expected = mib.Declarations.mind_nparams - num_params in if not (Int.equal (List.length params) expected) then - user_err "suppose it is" + user_err ~hdr:"suppose it is" (str "Wrong number of extra arguments: " ++ (if Int.equal expected 0 then str "none" else int expected) ++ spc () ++ str "expected.") in @@ -348,7 +348,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps = Thesis (Plain) -> Glob_term.GSort(Loc.ghost,GProp) | Thesis (For rec_occ) -> if not (Id.List.mem rec_occ pat_vars) then - user_err "suppose it is" + user_err ~hdr:"suppose it is" (str "Variable " ++ Nameops.pr_id rec_occ ++ str " does not occur in pattern."); Glob_term.GSort(Loc.ghost,GProp) diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 9510ba384..4649b1005 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -43,7 +43,7 @@ let clear ids { it = goal; sigma } = let (hyps, concl) = try Evarutil.clear_hyps_in_evi env evdref sign cl ids with Evarutil.ClearDependencyError (id, _) -> - user_err "" (str "Cannot clear " ++ pr_id id) + user_err (str "Cannot clear " ++ pr_id id) in let sigma = !evdref in let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in @@ -1082,12 +1082,12 @@ let thesis_for obj typ per_info env= let cind,all_args=decompose_app typ in let ind,u = destInd cind in let _ = if not (eq_ind ind per_info.per_ind) then - user_err "thesis_for" + user_err ~hdr:"thesis_for" ((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++ str"cannot give an induction hypothesis (wrong inductive type).") in let params,args = List.chop per_info.per_nparams all_args in let _ = if not (List.for_all2 eq_constr params per_info.per_params) then - user_err "thesis_for" + user_err ~hdr:"thesis_for" ((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++ str "cannot give an induction hypothesis (wrong parameters).") in let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 3c26c4710..5e7d810c9 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -293,7 +293,7 @@ let pr_long_global ref = pr_path (Nametab.path_of_global ref) (*S Warning and Error messages. *) -let err s = user_err "Extraction" s +let err s = user_err ~hdr:"Extraction" s let warn_extraction_axiom_to_realize = CWarnings.create ~name:"extraction-axiom-to-realize" ~category:"extraction" diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index f4daa0323..718448fc1 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -609,7 +609,7 @@ let build_scheme fas = try Smartlocate.global_with_alias f with Not_found -> - user_err "FunInd.build_scheme" + user_err ~hdr:"FunInd.build_scheme" (str "Cannot find " ++ Libnames.pr_reference f) in let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in @@ -643,7 +643,7 @@ let build_case_scheme fa = let (_,f,_) = fa in try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f)) with Not_found -> - user_err "FunInd.build_case_scheme" + user_err ~hdr:"FunInd.build_case_scheme" (str "Cannot find " ++ Libnames.pr_reference f) in let first_fun,u = destConst funs in let funs_mp,funs_dp,_ = Names.repr_con first_fun in diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 9902b0128..56ba0cba9 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -630,7 +630,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let (ind,_) = try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> - user_err "" (str "Cannot find the inductive associated to " ++ + user_err (str "Cannot find the inductive associated to " ++ Printer.pr_glob_constr b ++ str " in " ++ Printer.pr_glob_constr rt ++ str ". try again with a cast") in @@ -662,7 +662,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let (ind,_) = try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> - user_err "" (str "Cannot find the inductive associated to " ++ + user_err (str "Cannot find the inductive associated to " ++ Printer.pr_glob_constr b ++ str " in " ++ Printer.pr_glob_constr rt ++ str ". try again with a cast") in @@ -1198,7 +1198,7 @@ let rec compute_cst_params relnames params = function | GSort _ -> params | GHole _ -> params | GIf _ | GRec _ | GCast _ -> - raise (UserError("compute_cst_params", str "Not handled case")) + raise (UserError(Some "compute_cst_params", str "Not handled case")) and compute_cst_params_from_app acc (params,rtl) = match params,rtl with | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *) diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 01e5ef7fb..4e561fc7e 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -406,7 +406,7 @@ let is_free_in id = | GIf(_,cond,_,br1,br2) -> is_free_in cond || is_free_in br1 || is_free_in br2 - | GRec _ -> raise (UserError("",str "Not handled GRec")) + | GRec _ -> raise (UserError(None,str "Not handled GRec")) | GSort _ -> false | GHole _ -> false | GCast (_,b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t @@ -502,7 +502,7 @@ let replace_var_by_term x_id term = replace_var_by_pattern lhs, replace_var_by_pattern rhs ) - | GRec _ -> raise (UserError("",str "Not handled GRec")) + | GRec _ -> raise (UserError(None,str "Not handled GRec")) | GSort _ -> rt | GHole _ -> rt | GCast(loc,b,c) -> @@ -655,7 +655,7 @@ let zeta_normalize = zeta_normalize_term lhs, zeta_normalize_term rhs ) - | GRec _ -> raise (UserError("",str "Not handled GRec")) + | GRec _ -> raise (UserError(None,str "Not handled GRec")) | GSort _ -> rt | GHole _ -> rt | GCast(loc,b,c) -> diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 943ebc9fc..61e31277f 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -42,7 +42,7 @@ let functional_induction with_clean c princl pat = let finfo = (* we first try to find out a graph on f *) try find_Function_infos c' with Not_found -> - user_err "" (str "Cannot find induction information on "++ + user_err (str "Cannot find induction information on "++ Printer.pr_lconstr (mkConst c') ) in match Tacticals.elimination_sort_of_goal g with @@ -70,11 +70,11 @@ let functional_induction with_clean c princl pat = (b,a) (* mkConst(const_of_id princ_name ),g (\* FIXME *\) *) with Not_found -> (* This one is neither defined ! *) - user_err "" (str "Cannot find induction principle for " + user_err (str "Cannot find induction principle for " ++Printer.pr_lconstr (mkConst c') ) in (princ,NoBindings, Tacmach.pf_unsafe_type_of g' princ,g') - | _ -> raise (UserError("",str "functional induction must be used with a function" )) + | _ -> raise (UserError(None,str "functional induction must be used with a function" )) end | Some ((princ,binding)) -> princ,binding,Tacmach.pf_unsafe_type_of g princ,g @@ -175,7 +175,7 @@ let build_newrecursive l = match body_opt with | Some body -> (fixna,bll,ar,body) - | None -> user_err "Function" (str "Body of Function must be given") + | None -> user_err ~hdr:"Function" (str "Body of Function must be given") ) l in build_newrecursive l' @@ -321,7 +321,7 @@ let error_error names e = in match e with | Building_graph e -> - user_err "" + user_err (str "Cannot define graph(s) for " ++ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ e_explain e) @@ -391,7 +391,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = match fixpoint_exprl with | [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec -> - let body = match body with | Some body -> body | None -> user_err "Function" (str "Body of Function must be given") in + let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in Command.do_definition fname (Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl @@ -630,7 +630,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof | _ -> assert false in let fixpoint_exprl = [fixpoint_expr] in - let body = match body with | Some body -> body | None -> user_err "Function" (str "Body of Function must be given") in + let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in let recdefs,rec_impls = build_newrecursive fixpoint_exprl in let using_lemmas = [] in let pre_hook pconstants = @@ -656,7 +656,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof let fixpoint_exprl = [fixpoint_expr] in let recdefs,rec_impls = build_newrecursive fixpoint_exprl in let using_lemmas = [] in - let body = match body with | Some body -> body | None -> user_err "Function" (str "Body of Function must be given") in + let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in let pre_hook pconstants = generate_principle (ref (Evd.from_env (Global.env ()))) @@ -834,9 +834,9 @@ let make_graph (f_ref:global_reference) = | ConstRef c -> begin try c,Global.lookup_constant c with Not_found -> - raise (UserError ("",str "Cannot find " ++ Printer.pr_lconstr (mkConst c)) ) + raise (UserError (None,str "Cannot find " ++ Printer.pr_lconstr (mkConst c)) ) end - | _ -> raise (UserError ("", str "Not a function reference") ) + | _ -> raise (UserError (None, str "Not a function reference") ) in (match Global.body_of_constant_body c_body with | None -> error "Cannot build a graph over an axiom !" diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index a1c94f8cb..a45effb16 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -49,7 +49,7 @@ let locate_constant ref = let locate_with_msg msg f x = try f x - with Not_found -> raise (CErrors.UserError("", msg)) + with Not_found -> raise (CErrors.UserError(None, msg)) let filter_map filter f = @@ -73,7 +73,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 (CErrors.UserError("chop_rlambda_n", + raise (CErrors.UserError(Some "chop_rlambda_n", str "chop_rlambda_n: Not enough Lambdas")) in chop_lambda_n [] @@ -85,7 +85,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 (CErrors.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products")) + | _ -> raise (CErrors.UserError(Some "chop_rprod_n",str "chop_rprod_n: Not enough products")) in chop_prod_n [] @@ -110,7 +110,7 @@ let const_of_id id = in try Constrintern.locate_reference princ_ref with Not_found -> - CErrors.user_err "IndFun.const_of_id" + CErrors.user_err ~hdr:"IndFun.const_of_id" (str "cannot find " ++ Nameops.pr_id id) let def_of_const t = diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index ee1232013..e86231ba9 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -998,7 +998,7 @@ let invfun qhyp f = let f = match f with | ConstRef f -> f - | _ -> raise (CErrors.UserError("",str "Not a function")) + | _ -> raise (CErrors.UserError(None,str "Not a function")) in try let finfos = find_Function_infos f in @@ -1043,19 +1043,19 @@ let invfun qhyp f g = functional_inversion kn hid f2 f_correct g with | Failure "" -> - user_err "" (str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function") + user_err (str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function") | Option.IsNone -> if do_observe () then error "Cannot use equivalence with graph for any side of the equality" - else user_err "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid) + else user_err (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid) | Not_found -> if do_observe () then error "No graph found for any side of equality" - else user_err "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid) + else user_err (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid) end - | _ -> user_err "" (Ppconstr.pr_id hid ++ str " must be an equality ") + | _ -> user_err (Ppconstr.pr_id hid ++ str " must be an equality ") end) qhyp end diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 0b93a909a..76c5afec6 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -901,7 +901,7 @@ let find_Function_infos_safe (id:Id.t): Indfun_common.function_info = locate_constant f_ref in try find_Function_infos (kn_of_id id) with Not_found -> - user_err "indfun" (Nameops.pr_id id ++ str " has no functional scheme") + user_err ~hdr:"indfun" (Nameops.pr_id id ++ str " has no functional scheme") (** [merge id1 id2 args1 args2 id] builds and declares a new inductive type called [id], representing the merged graphs of both graphs diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 7745e8498..19c6ec8f4 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -307,7 +307,7 @@ let check_not_nested forbidden e = | Rel _ -> () | Var x -> if Id.List.mem x forbidden - then user_err "Recdef.check_not_nested" + then user_err ~hdr:"Recdef.check_not_nested" (str "check_not_nested: failure " ++ pr_id x) | Meta _ | Evar _ | Sort _ -> () | Cast(e,_,t) -> check_not_nested e;check_not_nested t @@ -327,7 +327,7 @@ let check_not_nested forbidden e = try check_not_nested e with UserError(_,p) -> - user_err "_" (str "on expr : " ++ Printer.pr_lconstr e ++ str " " ++ p) + user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_lconstr e ++ str " " ++ p) (* ['a info] contains the local information for traveling *) type 'a infos = @@ -442,7 +442,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) = check_not_nested (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; jinfo.otherS () expr_info continuation_tac expr_info with e when CErrors.noncritical e -> - user_err "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id) + user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id) end | Lambda(n,t,b) -> begin @@ -450,7 +450,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) = check_not_nested (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; jinfo.otherS () expr_info continuation_tac expr_info with e when CErrors.noncritical e -> - user_err "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id) + user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id) end | Case(ci,t,a,l) -> begin @@ -478,7 +478,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) = jinfo.apP (f,args) expr_info continuation_tac in travel_args jinfo expr_info.is_main_branch new_continuation_tac new_infos - | Case _ -> user_err "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)") + | Case _ -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)") | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_lconstr expr_info.info) end | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} @@ -723,8 +723,8 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = (List.map_i (fun i e -> observe_tac (str "do treat case") (treat_case f_is_present to_thin_intro (next_step continuation_tac) ci.ci_cstr_ndecls.(i) e new_info)) 0 (Array.to_list l) )) with - | UserError("Refiner.thensn_tac3",_) - | UserError("Refiner.tclFAIL_s",_) -> + | UserError(Some "Refiner.thensn_tac3",_) + | UserError(Some "Refiner.tclFAIL_s",_) -> (observe_tac (str "is computable " ++ Printer.pr_lconstr new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} ) )) g diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 9cfcb0fb7..367a13333 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -263,7 +263,7 @@ let rtauto_tac gls= let _= if Retyping.get_sort_family_of (pf_env gls) (Tacmach.project gls) gl != InProp - then user_err "rtauto" (Pp.str "goal should be in Prop") in + then user_err ~hdr:"rtauto" (Pp.str "goal should be in Prop") in let glf=make_form gamma gls gl in let hyps=make_hyps gamma gls [gl] (pf_hyps gls) in let formula= @@ -282,7 +282,7 @@ let rtauto_tac gls= let prf = try project (search_fun (init_state [] formula)) with Not_found -> - user_err "rtauto" (Pp.str "rtauto couldn't find any proof") in + user_err ~hdr:"rtauto" (Pp.str "rtauto couldn't find any proof") in let search_end_time = System.get_time () in let _ = if !verbose then begin diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 7450aa23e..a5e2211d8 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -79,7 +79,7 @@ let add_map s m = protect_maps := String.Map.add s m !protect_maps let lookup_map map = try String.Map.find map !protect_maps with Not_found -> - user_err"lookup_map"(str"map "++qs map++str"not found") + user_err ~hdr:"lookup_map" (str"map "++qs map++str"not found") let protect_red map env sigma c = kl (create_clos_infos all env) @@ -348,13 +348,13 @@ let find_ring_structure env sigma l = let check c = let ty' = Retyping.get_type_of env sigma c in if not (Reductionops.is_conv env sigma ty ty') then - user_err "ring" + user_err ~hdr:"ring" (str"arguments of ring_simplify do not have all the same type") in List.iter check cl'; (try ring_for_carrier ty with Not_found -> - user_err "ring" + user_err ~hdr:"ring" (str"cannot find a declared ring structure over"++ spc()++str"\""++pr_constr ty++str"\"")) | [] -> assert false @@ -828,13 +828,13 @@ let find_field_structure env sigma l = let check c = let ty' = Retyping.get_type_of env sigma c in if not (Reductionops.is_conv env sigma ty ty') then - user_err "field" + user_err ~hdr:"field" (str"arguments of field_simplify do not have all the same type") in List.iter check cl'; (try field_for_carrier ty with Not_found -> - user_err "field" + user_err ~hdr:"field" (str"cannot find a declared field structure over"++ spc()++str"\""++pr_constr ty++str"\"")) | [] -> assert false diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 199c26363..5fb0bb664 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -61,8 +61,8 @@ DECLARE PLUGIN "ssrmatching_plugin" type loc = Loc.t let dummy_loc = Loc.ghost -let errorstrm = CErrors.user_err "ssrmatching" -let loc_error loc msg = CErrors.user_err ~loc msg (str msg) +let errorstrm = CErrors.user_err ~hdr:"ssrmatching" +let loc_error loc msg = CErrors.user_err ~loc ~hdr:msg (str msg) let ppnl = Feedback.msg_info (* 0 cost pp function. Active only if env variable SSRDEBUG is set *) diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index c6fe553c5..ed8cc6ab0 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -52,7 +52,7 @@ let interp_ascii_string dloc s = if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2] then int_of_string s else - user_err ~loc:dloc "interp_ascii_string" + user_err ~loc:dloc ~hdr:"interp_ascii_string" (str "Expects a single character or a three-digits ascii code.") in interp_ascii dloc p diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index 6d62496ee..ab262fea7 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -47,7 +47,7 @@ let nat_of_int dloc n = mk_nat ref_O n end else - user_err "nat_of_int" + user_err ~hdr:"nat_of_int" (str "Cannot interpret a negative number as a number of type nat") (************************************************************************) diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index ac28714f5..a25ddb062 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -100,7 +100,7 @@ let int31_of_pos_bigint dloc n = GApp (dloc, ref_construct, List.rev (args 31 n)) let error_negative dloc = - CErrors.user_err ~loc:dloc "interp_int31" (Pp.str "int31 are only non-negative numbers.") + CErrors.user_err ~loc:dloc ~hdr:"interp_int31" (Pp.str "int31 are only non-negative numbers.") let interp_int31 dloc n = if is_pos_or_zero n then @@ -189,7 +189,7 @@ let bigN_of_pos_bigint dloc n = GApp (dloc, ref_constructor, args) let bigN_error_negative dloc = - CErrors.user_err ~loc:dloc "interp_bigN" (Pp.str "bigN are only non-negative numbers.") + CErrors.user_err ~loc:dloc ~hdr:"interp_bigN" (Pp.str "bigN are only non-negative numbers.") let interp_bigN dloc n = if is_pos_or_zero n then diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index 851ea3b74..b7b5fb8a5 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -57,7 +57,7 @@ let pos_of_bignat dloc x = pos_of x let error_non_positive dloc = - user_err ~loc:dloc "interp_positive" + user_err ~loc:dloc ~hdr:"interp_positive" (str "Only strictly positive numbers in type \"positive\".") let interp_positive dloc n = @@ -113,7 +113,7 @@ let n_of_binnat dloc pos_or_neg n = GRef (dloc, glob_N0, None) let error_negative dloc = - user_err ~loc:dloc "interp_N" (str "No negative numbers in type \"N\".") + user_err ~loc:dloc ~hdr:"interp_N" (str "No negative numbers in type \"N\".") let n_of_int dloc n = if is_pos_or_zero n then n_of_binnat dloc true n -- cgit v1.2.3