aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/auto_ind_decl.ml10
-rw-r--r--toplevel/class.ml8
-rw-r--r--toplevel/classes.ml7
-rw-r--r--toplevel/command.ml16
-rw-r--r--toplevel/coqinit.ml4
-rw-r--r--toplevel/ind_tables.ml2
-rw-r--r--toplevel/indschemes.ml2
-rw-r--r--toplevel/locality.ml2
-rw-r--r--toplevel/metasyntax.ml18
-rw-r--r--toplevel/mltop.ml10
-rw-r--r--toplevel/obligations.ml10
-rw-r--r--toplevel/record.ml10
-rw-r--r--toplevel/vernac.ml2
-rw-r--r--toplevel/vernacentries.ml42
-rw-r--r--toplevel/vernacinterp.ml4
15 files changed, 74 insertions, 73 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index d6c2ccad2..4f3eeda3a 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -340,7 +340,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
let rec find i =
if Id.equal avoid.(n-i) s then avoid.(n-i-x)
else (if i<n then find (i+1)
- else user_err "AutoIndDecl.do_replace_lb"
+ else user_err ~hdr:"AutoIndDecl.do_replace_lb"
(str "Var " ++ pr_id s ++ str " seems unknown.")
)
in mkVar (find 1)
@@ -398,7 +398,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
let rec find i =
if Id.equal avoid.(n-i) s then avoid.(n-i-x)
else (if i<n then find (i+1)
- else user_err "AutoIndDecl.do_replace_bl"
+ else user_err ~hdr:"AutoIndDecl.do_replace_bl"
(str "Var " ++ pr_id s ++ str " seems unknown.")
)
in mkVar (find 1)
@@ -506,7 +506,7 @@ let eqI ind l =
(List.map (fun (_,seq,_,_)-> mkVar seq) list_id ))
and e, eff =
try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff
- with Not_found -> user_err "AutoIndDecl.eqI"
+ with Not_found -> user_err ~hdr:"AutoIndDecl.eqI"
(str "The boolean equality on " ++ pr_mind (fst ind) ++ str " is needed.");
in (if Array.equal eq_constr eA [||] then e else mkApp(e,eA)), eff
@@ -633,7 +633,7 @@ let side_effect_of_mode = function
let make_bl_scheme mode mind =
let mib = Global.lookup_mind mind in
if not (Int.equal (Array.length mib.mind_packets) 1) then
- user_err ""
+ user_err
(str "Automatic building of boolean->Leibniz lemmas not supported");
let ind = (mind,0) in
let nparams = mib.mind_nparams in
@@ -756,7 +756,7 @@ let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined")
let make_lb_scheme mode mind =
let mib = Global.lookup_mind mind in
if not (Int.equal (Array.length mib.mind_packets) 1) then
- user_err ""
+ user_err
(str "Automatic building of Leibniz->boolean lemmas not supported");
let ind = (mind,0) in
let nparams = mib.mind_nparams in
diff --git a/toplevel/class.ml b/toplevel/class.ml
index bf17867e8..0dc799014 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -98,7 +98,7 @@ let class_of_global = function
| IndRef sp -> CL_IND sp
| VarRef id -> CL_SECVAR id
| ConstructRef _ as c ->
- user_err "class_of_global"
+ user_err ~hdr:"class_of_global"
(str "Constructors, such as " ++ Printer.pr_global c ++
str ", cannot be used as a class.")
@@ -177,7 +177,7 @@ let ident_key_of_class = function
(* Identity coercion *)
let error_not_transparent source =
- user_err "build_id_coercion"
+ user_err ~hdr:"build_id_coercion"
(pr_class source ++ str " must be a transparent constant.")
let build_id_coercion idf_opt source poly =
@@ -208,7 +208,7 @@ let build_id_coercion idf_opt source poly =
(Reductionops.is_conv_leq env sigma
(Typing.unsafe_type_of env sigma val_f) typ_f)
then
- user_err "" (strbrk
+ user_err (strbrk
"Cannot be defined as coercion (maybe a bad number of arguments).")
in
let idf =
@@ -284,7 +284,7 @@ let add_new_coercion_core coef stre poly source target isid =
let try_add_new_coercion_core ref ~local c d e f =
try add_new_coercion_core ref (loc_of_bool local) c d e f
with CoercionError e ->
- user_err "try_add_new_coercion_core"
+ user_err ~hdr:"try_add_new_coercion_core"
(explain_coercion_error ref e ++ str ".")
let try_add_new_coercion ref ~local poly =
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 6d62ce24a..cff744534 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -66,8 +66,9 @@ let existing_instance glob g pri =
match class_of_constr r with
| Some (_, ((tc,u), _)) -> add_instance (new_instance tc pri glob
(*FIXME*) (Flags.use_polymorphic_flag ()) c)
- | None -> user_err ~loc:(loc_of_reference g) "declare_instance"
- (Pp.str "Constant does not build instances of a declared type class.")
+ | None -> user_err ~loc:(loc_of_reference g)
+ ~hdr:"declare_instance"
+ (Pp.str "Constant does not build instances of a declared type class.")
let mismatched_params env n m = mismatched_ctx_inst env Parameters n m
let mismatched_props env n m = mismatched_ctx_inst env Properties n m
@@ -169,7 +170,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
Name id ->
let sp = Lib.make_path id in
if Nametab.exists_cci sp then
- user_err "new_instance" (Nameops.pr_id id ++ Pp.str " already exists.");
+ user_err ~hdr:"new_instance" (Nameops.pr_id id ++ Pp.str " already exists.");
id
| Anonymous ->
let i = Nameops.add_suffix (id_of_class k) "_instance_0" in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 4d333c30d..c8e0d1637 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -57,7 +57,7 @@ let rec complete_conclusion a cs = function
| CHole (loc, k, _, _) ->
let (has_no_args,name,params) = a in
if not has_no_args then
- user_err ~loc ""
+ user_err ~loc
(strbrk"Cannot infer the non constant arguments of the conclusion of "
++ pr_id cs ++ str ".");
let args = List.map (fun id -> CRef(Ident(loc,id),None)) params in
@@ -330,7 +330,7 @@ let do_assumptions kind nl l = match l with
| (Discharge, _, _) when Lib.sections_are_opened () ->
let loc = fst id in
let msg = Pp.str "Section variables cannot be polymorphic." in
- user_err ~loc "" msg
+ user_err ~loc msg
| _ -> ()
in
do_assumptions_bound_univs coe kind nl id (Some pl) c
@@ -342,7 +342,7 @@ let do_assumptions kind nl l = match l with
let loc = fst id in
let msg =
Pp.str "Assumptions with bound universes can only be defined one at a time." in
- user_err ~loc "" msg
+ user_err ~loc msg
in
(coe, (List.map map idl, c))
in
@@ -438,7 +438,7 @@ let interp_ind_arity env evdref ind =
let t, impls = understand_tcc_evars env evdref ~expected_type:IsType c, imps in
let pseudo_poly = check_anonymous_type c in
let () = if not (Reduction.is_arity env t) then
- user_err ~loc:(constr_loc ind.ind_arity) "" (str "Not an arity")
+ user_err ~loc:(constr_loc ind.ind_arity) (str "Not an arity")
in
t, pseudo_poly, impls
@@ -553,7 +553,7 @@ let check_named (loc, na) = match na with
| Name _ -> ()
| Anonymous ->
let msg = str "Parameters must be named." in
- user_err ~loc "" msg
+ user_err ~loc msg
let check_param = function
@@ -955,7 +955,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let relargty =
let error () =
user_err ~loc:(constr_loc r)
- "Command.build_wellfounded"
+ ~hdr:"Command.build_wellfounded"
(Printer.pr_constr_env env !evdref rel ++ str " is not an homogeneous binary relation.")
in
try
@@ -1312,7 +1312,7 @@ let do_program_fixpoint local poly l =
match n with
| Some n -> mkIdentC (snd n)
| None ->
- user_err "do_program_fixpoint"
+ user_err ~hdr:"do_program_fixpoint"
(str "Recursive argument required for well-founded fixpoints")
in build_wellfounded (id, pl, n, bl, typ, out_def def) poly r recarg ntn
@@ -1326,7 +1326,7 @@ let do_program_fixpoint local poly l =
do_program_recursive local poly fixkind fixl ntns
| _, _ ->
- user_err "do_program_fixpoint"
+ user_err ~hdr:"do_program_fixpoint"
(str "Well-founded fixpoints not allowed in mutually recursive blocks")
let check_safe () =
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index b90e62048..59ee95b31 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -136,7 +136,7 @@ let get_compat_version = function
| "8.3" -> Flags.V8_3
| "8.2" -> Flags.V8_2
| ("8.1" | "8.0") as s ->
- CErrors.user_err "get_compat_version"
+ CErrors.user_err ~hdr:"get_compat_version"
(str "Compatibility with version " ++ str s ++ str " not supported.")
- | s -> CErrors.user_err "get_compat_version"
+ | s -> CErrors.user_err ~hdr:"get_compat_version"
(str "Unknown compatibility version \"" ++ str s ++ str "\".")
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index fee5cffeb..85d0b6194 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -87,7 +87,7 @@ let declare_scheme_object s aux f =
try
let _ = Hashtbl.find scheme_object_table key in
(* let aux_msg = if aux="" then "" else " (with key "^aux^")" in*)
- user_err "IndTables.declare_scheme_object"
+ user_err ~hdr:"IndTables.declare_scheme_object"
(str "Scheme object " ++ str key ++ str " already declared.")
with Not_found ->
Hashtbl.add scheme_object_table key (s,f);
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index f9e6c207c..e0b861e0a 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -193,7 +193,7 @@ let try_declare_scheme what f internal names kn =
in
match msg with
| None -> ()
- | Some msg -> iraise (UserError ("", msg), snd e)
+ | Some msg -> iraise (UserError (None, msg), snd e)
let beq_scheme_msg mind =
let mib = Global.lookup_mind mind in
diff --git a/toplevel/locality.ml b/toplevel/locality.ml
index 7664acbb6..03640676e 100644
--- a/toplevel/locality.ml
+++ b/toplevel/locality.ml
@@ -18,7 +18,7 @@ let check_locality locality_flag =
match locality_flag with
| Some b ->
let s = if b then "Local" else "Global" in
- CErrors.user_err "Locality.check_locality"
+ CErrors.user_err ~hdr:"Locality.check_locality"
(str "This command does not support the \"" ++ str s ++ str "\" prefix.")
| None -> ()
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index cef074699..cd244bf63 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -238,7 +238,7 @@ let rec find_pattern nt xl = function
| _, Break s :: _ | Break s :: _, _ ->
error ("A break occurs on one side of \"..\" but not on the other side.")
| _, Terminal s :: _ | Terminal s :: _, _ ->
- user_err "Metasyntax.find_pattern"
+ user_err ~hdr:"Metasyntax.find_pattern"
(str "The token \"" ++ str s ++ str "\" occurs on one side of \"..\" but not on the other side.")
| _, [] ->
error msg_expected_form_of_recursive_notation
@@ -300,7 +300,7 @@ let rec get_notation_vars = function
let vars = get_notation_vars sl in
if Id.equal id ldots_var then vars else
if Id.List.mem id vars then
- user_err "Metasyntax.get_notation_vars"
+ user_err ~hdr:"Metasyntax.get_notation_vars"
(str "Variable " ++ pr_id id ++ str " occurs more than once.")
else
id::vars
@@ -314,7 +314,7 @@ let analyze_notation_tokens l =
recvars, List.subtract Id.equal vars (List.map snd recvars), l
let error_not_same_scope x y =
- user_err "Metasyntax.error_not_name_scope"
+ user_err ~hdr:"Metasyntax.error_not_name_scope"
(str "Variables " ++ pr_id x ++ str " and " ++ pr_id y ++ str " must be in the same scope.")
(**********************************************************************)
@@ -390,7 +390,7 @@ let check_open_binder isopen sl m =
| _ -> assert false
in
if isopen && not (List.is_empty sl) then
- user_err "" (str "as " ++ pr_id m ++
+ user_err (str "as " ++ pr_id m ++
str " is a non-closed binder, no such \"" ++
prlist_with_sep spc pr_token sl
++ strbrk "\" is allowed to occur.")
@@ -661,7 +661,7 @@ let pr_level ntn (from,args) =
prlist_with_sep pr_comma (pr_arg_level from) args
let error_incompatible_level ntn oldprec prec =
- user_err ""
+ user_err
(str "Notation " ++ str ntn ++ str " is already defined" ++ spc() ++
pr_level ntn oldprec ++
spc() ++ str "while it is now required to be" ++ spc() ++
@@ -731,7 +731,7 @@ let interp_modifiers modl =
| SetEntryType (s,typ) :: l ->
let id = Id.of_string s in
if Id.List.mem_assoc id etyps then
- user_err "Metasyntax.interp_modifiers"
+ user_err ~hdr:"Metasyntax.interp_modifiers"
(str s ++ str " is already assigned to an entry or constr level.");
interp assoc level ((id,typ)::etyps) format extra l
| SetItemLevel ([],n) :: l ->
@@ -739,7 +739,7 @@ let interp_modifiers modl =
| SetItemLevel (s::idl,n) :: l ->
let id = Id.of_string s in
if Id.List.mem_assoc id etyps then
- user_err "Metasyntax.interp_modifiers"
+ user_err ~hdr:"Metasyntax.interp_modifiers"
(str s ++ str " is already assigned to an entry or constr level.");
let typ = ETConstr (n,()) in
interp assoc level ((id,typ)::etyps) format extra (SetItemLevel (idl,n)::l)
@@ -770,7 +770,7 @@ let check_infix_modifiers modifiers =
let check_useless_entry_types recvars mainvars etyps =
let vars = let (l1,l2) = List.split recvars in l1@l2@mainvars in
match List.filter (fun (x,etyp) -> not (List.mem x vars)) etyps with
- | (x,_)::_ -> user_err "Metasyntax.check_useless_entry_types"
+ | (x,_)::_ -> user_err ~hdr:"Metasyntax.check_useless_entry_types"
(pr_id x ++ str " is unbound in the notation.")
| _ -> ()
@@ -813,7 +813,7 @@ let join_auxiliary_recursive_types recvars etyps =
| None, Some ytyp -> (x,ytyp)::typs
| Some xtyp, Some ytyp when Pervasives.(=) xtyp ytyp -> typs (* FIXME *)
| Some xtyp, Some ytyp ->
- user_err ""
+ user_err
(strbrk "In " ++ pr_id x ++ str " .. " ++ pr_id y ++
strbrk ", both ends have incompatible types."))
recvars etyps
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index c74c3522d..f9e0bc34a 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -124,13 +124,13 @@ let ml_load s =
| (UserError _ | Failure _ | Not_found as u) -> Exninfo.iraise (u, snd e)
| exc ->
let msg = report_on_load_obj_error exc in
- user_err "Mltop.load_object" (str"Cannot link ml-object " ++
+ user_err ~hdr:"Mltop.load_object" (str"Cannot link ml-object " ++
str s ++ str" to Coq code (" ++ msg ++ str ")."))
| WithoutTop ->
try
Dynlink.loadfile s; s
with Dynlink.Error a ->
- user_err "Mltop.load_object"
+ user_err ~hdr:"Mltop.load_object"
(strbrk "while loading " ++ str s ++
strbrk ": " ++ str (Dynlink.error_message a))
@@ -151,7 +151,7 @@ let dir_ml_use s =
if Dynlink.is_native then " Loading ML code works only in bytecode."
else ""
in
- user_err "Mltop.dir_ml_use" (str "Could not load ML code." ++ str moreinfo)
+ user_err ~hdr:"Mltop.dir_ml_use" (str "Could not load ML code." ++ str moreinfo)
(* Adds a path to the ML paths *)
let add_ml_dir s =
@@ -221,7 +221,7 @@ let get_ml_object_suffix name =
let file_of_name name =
let suffix = get_ml_object_suffix name in
let fail s =
- user_err "Mltop.load_object"
+ user_err ~hdr:"Mltop.load_object"
(str"File not found on loadpath : " ++ str s ++ str"\n" ++
str"Loadpath: " ++ str(String.concat ":" !coq_mlpath_copy)) in
if not (Filename.is_relative name) then
@@ -355,7 +355,7 @@ let trigger_ml_object verb cache reinit ?path name =
add_loaded_module name (known_module_path name);
if cache then perform_cache_obj name
end else if not has_dynlink then
- user_err "Mltop.trigger_ml_object"
+ user_err ~hdr:"Mltop.trigger_ml_object"
(str "Dynamic link not supported (module " ++ str name ++ str ")")
else begin
let file = file_of_name (Option.default name path) in
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index b9fd2894d..91704585a 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -258,7 +258,7 @@ let safe_init_constant md name () =
Coqlib.gen_constant "Obligations" md name
let hide_obligation = safe_init_constant tactics_module "obligation"
-let pperror cmd = CErrors.user_err "Program" cmd
+let pperror cmd = CErrors.user_err ~hdr:"Program" cmd
let error s = pperror (str s)
let reduce c =
@@ -398,7 +398,7 @@ let rec prod_app t n =
| Prod (_,_,b) -> subst1 n b
| LetIn (_, b, t, b') -> prod_app (subst1 b b') n
| _ ->
- user_err "prod_app"
+ user_err ~hdr:"prod_app"
(str"Needed a product, but didn't find one" ++ fnl ())
@@ -444,7 +444,7 @@ let from_prg : program_info ProgMap.t ref =
let close sec =
if not (ProgMap.is_empty !from_prg) then
let keys = map_keys !from_prg in
- user_err "Program"
+ user_err ~hdr:"Program"
(str "Unsolved obligations when closing " ++ str sec ++ str":" ++ spc () ++
prlist_with_sep spc (fun x -> Nameops.pr_id x) keys ++
(str (if Int.equal (List.length keys) 1 then " has " else " have ") ++
@@ -718,7 +718,7 @@ let get_prog name =
let progs = Id.Set.elements (ProgMap.domain prg_infos) in
let prog = List.hd progs in
let progs = prlist_with_sep pr_comma Nameops.pr_id progs in
- user_err ""
+ user_err
(str "More than one program with unsolved obligations: " ++ progs
++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Nameops.pr_id prog ++ str "\""))
@@ -985,7 +985,7 @@ and solve_obligation_by_tac prg obls i tac =
let (e, _) = CErrors.push e in
match e with
| Refiner.FailError (_, s) ->
- user_err ~loc:(fst obl.obl_location) "solve_obligation" (Lazy.force s)
+ user_err ~loc:(fst obl.obl_location) ~hdr:"solve_obligation" (Lazy.force s)
| e -> None (* FIXME really ? *)
and solve_prg_obligations prg ?oblset tac =
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 22dc8c957..219f078e1 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -102,7 +102,7 @@ let typecheck_params_and_fields def id pl t ps nots fs =
let error bk (loc, name) =
match bk, name with
| Default _, Anonymous ->
- user_err ~loc "record" (str "Record parameters must be named")
+ user_err ~loc ~hdr:"record" (str "Record parameters must be named")
| _ -> ()
in
List.iter
@@ -127,7 +127,7 @@ let typecheck_params_and_fields def id pl t ps nots fs =
sred, true
| None -> s, false
else s, false)
- | _ -> user_err ~loc:(constr_loc t) "" (str"Sort expected."))
+ | _ -> user_err ~loc:(constr_loc t) (str"Sort expected."))
| None ->
let uvarkind = Evd.univ_flexible_alg in
mkSort (Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars), true
@@ -208,7 +208,7 @@ let warning_or_error coe indsp err =
| _ ->
(pr_id fi ++ strbrk " cannot be defined because it is not typable.")
in
- if coe then user_err "structure" st;
+ if coe then user_err ~hdr:"structure" st;
Flags.if_verbose Feedback.msg_info (hov 0 st)
type field_status =
@@ -235,7 +235,7 @@ let subst_projection fid l c =
| Projection t -> lift depth t
| NoProjection (Name id) -> bad_projs := id :: !bad_projs; mkRel k
| NoProjection Anonymous ->
- user_err "" (str "Field " ++ pr_id fid ++
+ user_err (str "Field " ++ pr_id fid ++
str " depends on the " ++ pr_nth (k-depth-1) ++ str
" field which has no name.")
else
@@ -539,7 +539,7 @@ let declare_existing_class g =
match g with
| ConstRef x -> add_constant_class x
| IndRef x -> add_inductive_class x
- | _ -> user_err "declare_existing_class"
+ | _ -> user_err ~hdr:"declare_existing_class"
(Pp.str"Unsupported class type, only constants and inductives are allowed")
open Vernacexpr
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 00655497b..d345b3229 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -70,7 +70,7 @@ let disable_drop = function
| Drop -> CErrors.error "Drop is forbidden."
| e -> e
-let user_error loc s = CErrors.user_err ~loc "_" (str s)
+let user_error loc s = CErrors.user_err ~loc ~hdr:"_" (str s)
(* Opening and closing a channel. Open it twice when verbose: the first
channel is used to read the commands, and the second one to print them.
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 9e3494145..3dd19fa1d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -381,7 +381,7 @@ let err_unmapped_library loc ?from qid =
str " and prefix " ++ pr_dirpath from ++ str "."
in
user_err ~loc
- "locate_library"
+ ~hdr:"locate_library"
(strbrk "Cannot find a physical path bound to logical path matching suffix " ++
pr_dirpath dir ++ prefix)
@@ -391,7 +391,7 @@ let err_notfound_library loc ?from qid =
| Some from ->
str " with prefix " ++ pr_dirpath from ++ str "."
in
- user_err ~loc "locate_library"
+ user_err ~loc ~hdr:"locate_library"
(strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix)
let print_located_library r =
@@ -483,7 +483,7 @@ let vernac_start_proof locality p kind l lettop =
| None -> ()) l;
if not(refining ()) then
if lettop then
- user_err "Vernacentries.StartProof"
+ user_err ~hdr:"Vernacentries.StartProof"
(str "Let declarations can only be used in proof editing mode.");
start_proof_and_print (local, p, Proof kind) l no_hook
@@ -604,14 +604,14 @@ let vernac_combined_scheme lid l =
let vernac_universe loc poly l =
if poly && not (Lib.sections_are_opened ()) then
- user_err ~loc "vernac_universe"
+ user_err ~loc ~hdr:"vernac_universe"
(str"Polymorphic universes can only be declared inside sections, " ++
str "use Monomorphic Universe instead");
do_universe poly l
let vernac_constraint loc poly l =
if poly && not (Lib.sections_are_opened ()) then
- user_err ~loc "vernac_constraint"
+ user_err ~loc ~hdr:"vernac_constraint"
(str"Polymorphic universe constraints can only be declared"
++ str " inside sections, use Monomorphic Constraint instead");
do_constraint poly l
@@ -855,7 +855,7 @@ let vernac_set_used_variables e =
let vars = Environ.named_context env in
List.iter (fun id ->
if not (List.exists (Id.equal id % get_id) vars) then
- user_err "vernac_set_used_variables"
+ user_err ~hdr:"vernac_set_used_variables"
(str "Unknown variable: " ++ pr_id id))
l;
let _, to_clear = set_used_variables l in
@@ -974,9 +974,9 @@ let vernac_declare_arguments locality r l nargs flags =
| [], Anonymous::ld, (Some _)::ls when extra_scope_flag -> check li ld ls
| [], _::_, (Some _)::ls when extra_scope_flag ->
error "Extra notation scopes can be set on anonymous arguments only"
- | [], x::_, _ -> user_err "vernac_declare_arguments"
+ | [], x::_, _ -> user_err ~hdr:"vernac_declare_arguments"
(str "Extra argument " ++ pr_name x ++ str ".")
- | l, [], _ -> user_err "vernac_declare_arguments"
+ | l, [], _ -> user_err ~hdr:"vernac_declare_arguments"
(str "The following arguments are not declared: " ++
prlist_with_sep pr_comma pr_name l ++ str ".")
| _::li, _::ld, _::ls -> check li ld ls
@@ -1019,7 +1019,7 @@ let vernac_declare_arguments locality r l nargs flags =
let sr', impl = List.fold_map (fun b -> function
| (Anonymous, _,_, true, max), Name id -> assert false
| (Name x, _,_, true, _), Anonymous ->
- user_err "vernac_declare_arguments"
+ user_err ~hdr:"vernac_declare_arguments"
(str "Argument " ++ pr_id x ++ str " cannot be declared implicit.")
| (Name iid, _,_, true, max), Name id ->
set_renamed iid id;
@@ -1033,7 +1033,7 @@ let vernac_declare_arguments locality r l nargs flags =
some_renaming_specified l in
if some_renaming_specified then
if not (List.mem `Rename flags) then
- user_err "vernac_declare_arguments"
+ user_err ~hdr:"vernac_declare_arguments"
(str "To rename arguments the \"rename\" flag must be specified." ++
match !renamed_arg with
| None -> mt ()
@@ -1077,7 +1077,7 @@ let vernac_declare_arguments locality r l nargs flags =
| ConstRef _ as c ->
Reductionops.ReductionBehaviour.set
(make_section_locality locality) c (rargs, nargs, flags)
- | _ -> user_err "" (strbrk "Modifiers of the behavior of the simpl tactic are relevant for constants only.")
+ | _ -> user_err (strbrk "Modifiers of the behavior of the simpl tactic are relevant for constants only.")
end;
if not (some_renaming_specified ||
some_implicits_specified ||
@@ -1498,7 +1498,7 @@ let print_about_hyp_globs ref_or_by_not glnumopt =
| Some n,AN (Ident (_loc,id)) -> (* goal number given, catch if wong *)
(try get_nth_goal n,id
with
- Failure _ -> user_err "print_about_hyp_globs"
+ Failure _ -> user_err ~hdr:"print_about_hyp_globs"
(str "No such goal: " ++ int n ++ str "."))
| _ , _ -> raise NoHyp in
let hyps = pf_hyps gl in
@@ -1574,7 +1574,7 @@ let global_module r =
let (loc,qid) = qualid_of_reference r in
try Nametab.full_name_module qid
with Not_found ->
- user_err ~loc "global_module"
+ user_err ~loc ~hdr:"global_module"
(str "Module/section " ++ pr_qualid qid ++ str " not found.")
let interp_search_restriction = function
@@ -1597,7 +1597,7 @@ let interp_search_about_item env =
(fun _ -> true) s sc in
GlobSearchSubPattern (Pattern.PRef ref)
with UserError _ ->
- user_err "interp_search_about_item"
+ user_err ~hdr:"interp_search_about_item"
(str "Unable to interp \"" ++ str s ++ str "\" either as a reference or as an identifier component")
let vernac_search s gopt r =
@@ -1877,12 +1877,12 @@ let interp ?proof ~loc locality poly c =
| VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n")
(* The STM should handle that, but LOAD bypasses the STM... *)
- | VernacAbort id -> CErrors.user_err "" (str "Abort cannot be used through the Load command")
- | VernacAbortAll -> CErrors.user_err "" (str "AbortAll cannot be used through the Load command")
- | VernacRestart -> CErrors.user_err "" (str "Restart cannot be used through the Load command")
- | VernacUndo _ -> CErrors.user_err "" (str "Undo cannot be used through the Load command")
- | VernacUndoTo _ -> CErrors.user_err "" (str "UndoTo cannot be used through the Load command")
- | VernacBacktrack _ -> CErrors.user_err "" (str "Backtrack cannot be used through the Load command")
+ | VernacAbort id -> CErrors.user_err (str "Abort cannot be used through the Load command")
+ | VernacAbortAll -> CErrors.user_err (str "AbortAll cannot be used through the Load command")
+ | VernacRestart -> CErrors.user_err (str "Restart cannot be used through the Load command")
+ | VernacUndo _ -> CErrors.user_err (str "Undo cannot be used through the Load command")
+ | VernacUndoTo _ -> CErrors.user_err (str "UndoTo cannot be used through the Load command")
+ | VernacBacktrack _ -> CErrors.user_err (str "Backtrack cannot be used through the Load command")
(* Proof management *)
| VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t,None)] false
@@ -2014,7 +2014,7 @@ let with_fail b f =
let (e, _) = CErrors.push e in
match e with
| HasNotFailed ->
- user_err "Fail" (str "The command has not failed!")
+ user_err ~hdr:"Fail" (str "The command has not failed!")
| HasFailed msg ->
if is_verbose () || !test_mode || !ide_slave then Feedback.msg_info
(str "The command has indeed failed with message:" ++ fnl () ++ msg)
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index 147727e7c..f26ef460d 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -22,7 +22,7 @@ let vinterp_add depr s f =
try
Hashtbl.add vernac_tab s (depr, f)
with Failure _ ->
- user_err "vinterp_add"
+ user_err ~hdr:"vinterp_add"
(str"Cannot add the vernac command " ++ str (fst s) ++ str" twice.")
let overwriting_vinterp_add s f =
@@ -37,7 +37,7 @@ let vinterp_map s =
try
Hashtbl.find vernac_tab s
with Failure _ | Not_found ->
- user_err "Vernac Interpreter"
+ user_err ~hdr:"Vernac Interpreter"
(str"Cannot find vernac command " ++ str (fst s) ++ str".")
let vinterp_init () = Hashtbl.clear vernac_tab
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 01:23:13 +0000