aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/classes.ml4
-rw-r--r--vernac/command.ml18
-rw-r--r--vernac/ind_tables.ml2
-rw-r--r--vernac/indschemes.ml6
-rw-r--r--vernac/lemmas.ml10
-rw-r--r--vernac/locality.ml10
-rw-r--r--vernac/metasyntax.ml68
-rw-r--r--vernac/record.ml2
-rw-r--r--vernac/vernacentries.ml78
9 files changed, 99 insertions, 99 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 5843da31e..004083dcf 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -353,7 +353,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
(match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) ();
id)
end
- else CErrors.error "Unsolved obligations remaining.")
+ else CErrors.user_err Pp.(str "Unsolved obligations remaining."))
let named_of_rel_context l =
let acc, ctx =
@@ -379,7 +379,7 @@ let context poly l =
let ctx =
try named_of_rel_context fullctx
with e when CErrors.noncritical e ->
- error "Anonymous variables not allowed in contexts."
+ user_err Pp.(str "Anonymous variables not allowed in contexts.")
in
let uctx = ref (Evd.universe_context_set !evars) in
let fn status (id, b, t) =
diff --git a/vernac/command.ml b/vernac/command.ml
index 8a9bbb884..4b29700e5 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -382,7 +382,7 @@ type structured_inductive_expr =
local_binder_expr list * structured_one_inductive_expr list
let minductive_message warn = function
- | [] -> error "No inductive definition."
+ | [] -> user_err Pp.(str "No inductive definition.")
| [x] -> (pr_id x ++ str " is defined" ++
if warn then str " as a non-primitive record" else mt())
| l -> hov 0 (prlist_with_sep pr_comma pr_id l ++
@@ -676,8 +676,8 @@ let extract_params indl =
match paramsl with
| [] -> anomaly (Pp.str "empty list of inductive types")
| params::paramsl ->
- if not (List.for_all (eq_local_binders params) paramsl) then error
- "Parameters should be syntactically the same for each inductive type.";
+ if not (List.for_all (eq_local_binders params) paramsl) then user_err Pp.(str
+ "Parameters should be syntactically the same for each inductive type.");
params
let extract_inductive indl =
@@ -715,9 +715,9 @@ let declare_mutual_inductive_with_eliminations mie pl impls =
begin match mie.mind_entry_finite with
| BiFinite when is_recursive mie ->
if Option.has_some mie.mind_entry_record then
- error "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command."
+ user_err Pp.(str "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command.")
else
- error ("Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command.")
+ user_err Pp.(str ("Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command."))
| _ -> ()
end;
let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
@@ -1122,7 +1122,7 @@ let interp_recursive isfix fixl notations =
| x , None -> x
| Some ls , Some us ->
if not (CList.for_all2eq (fun x y -> Id.equal (snd x) (snd y)) ls us) then
- error "(co)-recursive definitions should all have the same universe binders";
+ user_err Pp.(str "(co)-recursive definitions should all have the same universe binders");
Some us) fixl None in
let ctx = Evd.make_evar_universe_context env all_universes in
let evdref = ref (Evd.from_ctx ctx) in
@@ -1262,8 +1262,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
let extract_decreasing_argument limit = function
| (na,CStructRec) -> na
| (na,_) when not limit -> na
- | _ -> error
- "Only structural decreasing is supported for a non-Program Fixpoint"
+ | _ -> user_err Pp.(str
+ "Only structural decreasing is supported for a non-Program Fixpoint")
let extract_fixpoint_components limit l =
let fixl, ntnl = List.split l in
@@ -1282,7 +1282,7 @@ let extract_cofixpoint_components l =
let out_def = function
| Some def -> def
- | None -> error "Program Fixpoint needs defined bodies."
+ | None -> user_err Pp.(str "Program Fixpoint needs defined bodies.")
let collect_evars_of_term evd c ty =
let evars = Evar.Set.union (Evd.evars_of_term c) (Evd.evars_of_term ty) in
diff --git a/vernac/ind_tables.ml b/vernac/ind_tables.ml
index c6588684a..f3259f1f3 100644
--- a/vernac/ind_tables.ml
+++ b/vernac/ind_tables.ml
@@ -81,7 +81,7 @@ let scheme_object_table =
let declare_scheme_object s aux f =
let () =
if not (Id.is_valid ("ind" ^ s)) then
- error ("Illegal induction scheme suffix: " ^ s)
+ user_err Pp.(str ("Illegal induction scheme suffix: " ^ s))
in
let key = if String.is_empty aux then s else aux in
try
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index b21e80bef..a78221301 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -418,7 +418,7 @@ let get_common_underlying_mutual_inductive = function
raise (RecursionSchemeError (NotMutualInScheme (ind,ind')))
| [] ->
if not (List.distinct_f Int.compare (List.map snd (List.map snd all)))
- then error "A type occurs twice";
+ then user_err Pp.(str "A type occurs twice");
mind,
List.map_filter
(function (Some id,(_,i)) -> Some (i,snd id) | (None,_) -> None) all
@@ -429,7 +429,7 @@ let do_scheme l =
tried to declare different schemes at once *)
if not (List.is_empty ischeme) && not (List.is_empty escheme)
then
- error "Do not declare equality and induction scheme at the same time."
+ user_err Pp.(str "Do not declare equality and induction scheme at the same time.")
else (
if not (List.is_empty ischeme) then do_mutual_induction_scheme ischeme
else
@@ -497,7 +497,7 @@ let do_combined_scheme name schemes =
let refe = Ident x in
let qualid = qualid_of_reference refe in
try Nametab.locate_constant (snd qualid)
- with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared."))
+ with Not_found -> user_err Pp.(pr_qualid (snd qualid) ++ str " is not declared."))
schemes
in
let body,typ = build_combined_scheme (Global.env ()) csts in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index c67a3302f..d6ae0ea86 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -153,9 +153,9 @@ let find_mutually_recursive_statements thms =
(* assume the largest indices as possible *)
List.last common_same_indhyp, false, possible_guards
| _, [] ->
- error
+ user_err Pp.(str
("Cannot find common (mutual) inductive premises or coinductive" ^
- " conclusions in the statements.")
+ " conclusions in the statements."))
in
(finite,guard,None), ordered_inds
@@ -273,7 +273,7 @@ let save_named ?export_seff proof =
let check_anonymity id save_ident =
if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then
- error "This command can only be used for unnamed theorem."
+ user_err Pp.(str "This command can only be used for unnamed theorem.")
let save_anonymous ?export_seff proof save_ident =
let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
@@ -478,10 +478,10 @@ let save_proof ?proof = function
match proof with
| Some ({ id; entries; persistence = k; universes }, _) ->
if List.length entries <> 1 then
- error "Admitted does not support multiple statements";
+ user_err Pp.(str "Admitted does not support multiple statements");
let { const_entry_secctx; const_entry_type } = List.hd entries in
if const_entry_type = None then
- error "Admitted requires an explicit statement";
+ user_err Pp.(str "Admitted requires an explicit statement");
let typ = Option.get const_entry_type in
let ctx = Evd.evar_context_universe_context (fst universes) in
let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
diff --git a/vernac/locality.ml b/vernac/locality.ml
index 03640676e..a25acb0d3 100644
--- a/vernac/locality.ml
+++ b/vernac/locality.ml
@@ -35,9 +35,9 @@ let enforce_locality_full locality_flag local =
let local =
match locality_flag with
| Some false when local ->
- CErrors.error "Cannot be simultaneously Local and Global."
+ CErrors.user_err Pp.(str "Cannot be simultaneously Local and Global.")
| Some true when local ->
- CErrors.error "Use only prefix \"Local\"."
+ CErrors.user_err Pp.(str "Use only prefix \"Local\".")
| None ->
if local then begin
warn_deprecated_local_syntax ();
@@ -66,7 +66,7 @@ let enforce_locality_exp locality_flag local =
| None, Some local -> local
| Some b, None -> local_of_bool b
| None, None -> Decl_kinds.Global
- | Some _, Some _ -> CErrors.error "Local non allowed in this case"
+ | Some _, Some _ -> CErrors.user_err Pp.(str "Local non allowed in this case")
(* For commands whose default is to not discharge but to export:
Global in sections forces discharge, Global not in section is the default;
@@ -87,8 +87,8 @@ let enforce_section_locality locality_flag local =
let make_module_locality = function
| Some false ->
if Lib.sections_are_opened () then
- CErrors.error
- "This command does not support the Global option in sections.";
+ CErrors.user_err Pp.(str
+ "This command does not support the Global option in sections.");
false
| Some true -> true
| None -> false
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index fb7c72941..42494dd28 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -60,7 +60,7 @@ let pr_entry e =
let pr_registered_grammar name =
let gram = try Some (String.Map.find name !grammars) with Not_found -> None in
match gram with
- | None -> error "Unknown or unprintable grammar entry."
+ | None -> user_err Pp.(str "Unknown or unprintable grammar entry.")
| Some entries ->
let pr_one (AnyEntry e) =
str "Entry " ++ str (Pcoq.Gram.Entry.name e) ++ str " is" ++ fnl () ++
@@ -107,11 +107,11 @@ let parse_format ((loc, str) : lstring) =
if Int.equal n 0 then l else push_token (UnpTerminal (String.make n ' ')) l in
let close_box i b = function
| a::(_::_ as l) -> push_token (UnpBox (b,a)) l
- | _ -> error "Non terminated box in format." in
+ | _ -> user_err Pp.(str "Non terminated box in format.") in
let close_quotation i =
if i < String.length str && str.[i] == '\'' && (Int.equal (i+1) l || str.[i+1] == ' ')
then i+1
- else error "Incorrectly terminated quoted expression." in
+ else user_err Pp.(str "Incorrectly terminated quoted expression.") in
let rec spaces n i =
if i < String.length str && str.[i] == ' ' then spaces (n+1) (i+1)
else n in
@@ -119,10 +119,10 @@ let parse_format ((loc, str) : lstring) =
if i < String.length str && str.[i] != ' ' then
if str.[i] == '\'' && quoted &&
(i+1 >= String.length str || str.[i+1] == ' ')
- then if Int.equal n 0 then error "Empty quoted token." else n
+ then if Int.equal n 0 then user_err Pp.(str "Empty quoted token.") else n
else nonspaces quoted (n+1) (i+1)
else
- if quoted then error "Spaces are not allowed in (quoted) symbols."
+ if quoted then user_err Pp.(str "Spaces are not allowed in (quoted) symbols.")
else n in
let rec parse_non_format i =
let n = nonspaces false 0 i in
@@ -153,8 +153,8 @@ let parse_format ((loc, str) : lstring) =
(* Parse " [ .. ", *)
| ' ' | '\'' ->
parse_box (fun n -> PpHOVB n) (i+1)
- | _ -> error "\"v\", \"hv\", \" \" expected after \"[\" in format."
- else error "\"v\", \"hv\" or \" \" expected after \"[\" in format."
+ | _ -> user_err Pp.(str "\"v\", \"hv\", \" \" expected after \"[\" in format.")
+ else user_err Pp.(str "\"v\", \"hv\" or \" \" expected after \"[\" in format.")
(* Parse "]" *)
| ']' ->
([] :: parse_token (close_quotation (i+1)))
@@ -165,7 +165,7 @@ let parse_format ((loc, str) : lstring) =
(parse_token (close_quotation (i+n))))
else
if Int.equal n 0 then []
- else error "Ending spaces non part of a format annotation."
+ else user_err Pp.(str "Ending spaces non part of a format annotation.")
and parse_box box i =
let n = spaces 0 i in
close_box i (box n) (parse_token (close_quotation (i+n)))
@@ -187,9 +187,9 @@ let parse_format ((loc, str) : lstring) =
try
if not (String.is_empty str) then match parse_token 0 with
| [l] -> l
- | _ -> error "Box closed without being opened in format."
+ | _ -> user_err Pp.(str "Box closed without being opened in format.")
else
- error "Empty format."
+ user_err Pp.(str "Empty format.")
with reraise ->
let (e, info) = CErrors.push reraise in
let info = Option.cata (Loc.add_loc info) info loc in
@@ -243,19 +243,19 @@ let rec find_pattern nt xl = function
| [], NonTerminal x' :: l' ->
(out_nt nt,x',List.rev xl),l'
| _, Break s :: _ | Break s :: _, _ ->
- error ("A break occurs on one side of \"..\" but not on the other side.")
+ user_err Pp.(str ("A break occurs on one side of \"..\" but not on the other side."))
| _, Terminal s :: _ | Terminal s :: _, _ ->
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
+ user_err Pp.(str msg_expected_form_of_recursive_notation)
| ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) ->
anomaly (Pp.str "Only Terminal or Break expected on left, non-SProdList on right")
let rec interp_list_parser hd = function
| [] -> [], List.rev hd
| NonTerminal id :: tl when Id.equal id ldots_var ->
- if List.is_empty hd then error msg_expected_form_of_recursive_notation;
+ if List.is_empty hd then user_err Pp.(str msg_expected_form_of_recursive_notation);
let hd = List.rev hd in
let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in
let xyl,tl'' = interp_list_parser [] tl' in
@@ -286,7 +286,7 @@ let quote_notation_token x =
let rec raw_analyze_notation_tokens = function
| [] -> []
| String ".." :: sl -> NonTerminal ldots_var :: raw_analyze_notation_tokens sl
- | String "_" :: _ -> error "_ must be quoted."
+ | String "_" :: _ -> user_err Pp.(str "_ must be quoted.")
| String x :: sl when CLexer.is_ident x ->
NonTerminal (Names.Id.of_string x) :: raw_analyze_notation_tokens sl
| String s :: sl ->
@@ -487,7 +487,7 @@ let make_hunks etyps symbols from =
(* Build default printing rules from explicit format *)
-let error_format () = error "The format does not match the notation."
+let error_format () = user_err Pp.(str "The format does not match the notation.")
let rec split_format_at_ldots hd = function
| UnpTerminal s :: fmt when String.equal s (Id.to_string ldots_var) -> List.rev hd, fmt
@@ -500,7 +500,7 @@ and check_no_ldots_in_box = function
| UnpBox (_,fmt) ->
(try
let _ = split_format_at_ldots [] fmt in
- error ("The special symbol \"..\" must occur at the same formatting depth than the variables of which it is the ellipse.")
+ user_err Pp.(str ("The special symbol \"..\" must occur at the same formatting depth than the variables of which it is the ellipse."))
with Exit -> ())
| _ -> ()
@@ -518,7 +518,7 @@ let read_recursive_format sl fmt =
let rec get_tail = function
| a :: sepfmt, b :: fmt when Pervasives.(=) a b -> get_tail (sepfmt, fmt) (* FIXME *)
| [], tail -> skip_var_in_recursive_format tail
- | _ -> error "The format is not the same on the right and left hand side of the special token \"..\"." in
+ | _ -> user_err Pp.(str "The format is not the same on the right and left hand side of the special token \"..\".") in
let slfmt, fmt = get_head fmt in
slfmt, get_tail (slfmt, fmt)
@@ -652,7 +652,7 @@ let make_production etyps symbols =
distribute
[GramConstrNonTerminal (ETBinderList (o,tkl), Some x)] ll
| _ ->
- error "Components of recursive patterns in notation must be terms or binders.")
+ user_err Pp.(str "Components of recursive patterns in notation must be terms or binders."))
symbols [[]] in
List.map define_keywords prod
@@ -811,7 +811,7 @@ let interp_modifiers modl = let open NotationMods in
interp { acc with level = Some n; } l
| SetAssoc a :: l ->
- if not (Option.is_empty acc.assoc) then error "An associativity is given more than once.";
+ if not (Option.is_empty acc.assoc) then user_err Pp.(str "An associativity is given more than once.");
interp { acc with assoc = Some a; } l
| SetOnlyParsing :: l ->
interp { acc with only_parsing = true; } l
@@ -820,7 +820,7 @@ let interp_modifiers modl = let open NotationMods in
| SetCompatVersion v :: l ->
interp { acc with compat = Some v; } l
| SetFormat ("text",s) :: l ->
- if not (Option.is_empty acc.format) then error "A format is given more than once.";
+ if not (Option.is_empty acc.format) then user_err Pp.(str "A format is given more than once.");
interp { acc with format = Some s; } l
| SetFormat (k,(_,s)) :: l ->
interp { acc with extra = (k,s)::acc.extra; } l
@@ -829,7 +829,7 @@ let interp_modifiers modl = let open NotationMods in
let check_infix_modifiers modifiers =
let t = (interp_modifiers modifiers).NotationMods.etyps in
if not (List.is_empty t) then
- error "Explicit entry level or type unexpected in infix notation."
+ user_err Pp.(str "Explicit entry level or type unexpected in infix notation.")
let check_useless_entry_types recvars mainvars etyps =
let vars = let (l1,l2) = List.split recvars in l1@l2@mainvars in
@@ -901,7 +901,7 @@ let internalization_type_of_entry_type = function
| ETBigint | ETReference -> NtnInternTypeConstr
| ETBinder _ -> NtnInternTypeBinder
| ETName -> NtnInternTypeIdent
- | ETPattern | ETOther _ -> error "Not supported."
+ | ETPattern | ETOther _ -> user_err Pp.(str "Not supported.")
| ETBinderList _ | ETConstrList _ -> assert false
let set_internalization_type typs =
@@ -917,7 +917,7 @@ let make_interpretation_type isrec isonlybinding = function
| NtnInternTypeConstr | NtnInternTypeIdent ->
if isonlybinding then NtnTypeOnlyBinder else NtnTypeConstr
| NtnInternTypeBinder when isrec -> NtnTypeBinderList
- | NtnInternTypeBinder -> error "Type binder is only for use in recursive notations for binders."
+ | NtnInternTypeBinder -> user_err Pp.(str "Type binder is only for use in recursive notations for binders.")
let make_interpretation_vars recvars allvars =
let eq_subscope (sc1, l1) (sc2, l2) =
@@ -938,9 +938,9 @@ let make_interpretation_vars recvars allvars =
let check_rule_productivity l =
if List.for_all (function NonTerminal _ | Break _ -> true | _ -> false) l then
- error "A notation must include at least one symbol.";
+ user_err Pp.(str "A notation must include at least one symbol.");
if (match l with SProdList _ :: _ -> true | _ -> false) then
- error "A recursive notation must start with at least one symbol."
+ user_err Pp.(str "A recursive notation must start with at least one symbol.")
let warn_notation_bound_to_variable =
CWarnings.create ~name:"notation-bound-to-variable" ~category:"parsing"
@@ -980,7 +980,7 @@ let find_precedence lev etyps symbols =
| Some (NonTerminal x) ->
(try match List.assoc x etyps with
| ETConstr _ ->
- error "The level of the leftmost non-terminal cannot be changed."
+ user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.")
| ETName | ETBigint | ETReference ->
begin match lev with
| None ->
@@ -988,31 +988,31 @@ let find_precedence lev etyps symbols =
| Some 0 ->
([],0)
| _ ->
- error "A notation starting with an atomic expression must be at level 0."
+ user_err Pp.(str "A notation starting with an atomic expression must be at level 0.")
end
| ETPattern | ETBinder _ | ETOther _ -> (* Give a default ? *)
if Option.is_empty lev then
- error "Need an explicit level."
+ user_err Pp.(str "Need an explicit level.")
else [],Option.get lev
| ETConstrList _ | ETBinderList _ ->
assert false (* internally used in grammar only *)
with Not_found ->
if Option.is_empty lev then
- error "A left-recursive notation must have an explicit level."
+ user_err Pp.(str "A left-recursive notation must have an explicit level.")
else [],Option.get lev)
| Some (Terminal _) when last_is_terminal () ->
if Option.is_empty lev then
([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."], 0)
else [],Option.get lev
| Some _ ->
- if Option.is_empty lev then error "Cannot determine the level.";
+ if Option.is_empty lev then user_err Pp.(str "Cannot determine the level.");
[],Option.get lev
let check_curly_brackets_notation_exists () =
try let _ = Notation.level_of_notation "{ _ }" in ()
with Not_found ->
- error "Notations involving patterns of the form \"{ _ }\" are treated \n\
-specially and require that the notation \"{ _ }\" is already reserved."
+ user_err Pp.(str "Notations involving patterns of the form \"{ _ }\" are treated \n\
+specially and require that the notation \"{ _ }\" is already reserved.")
(* Remove patterns of the form "{ _ }", unless it is the "{ _ }" notation *)
let remove_curly_brackets l =
@@ -1081,7 +1081,7 @@ let compute_syntax_data df modifiers =
let mods = interp_modifiers modifiers in
let onlyprint = mods.only_printing in
let onlyparse = mods.only_parsing in
- if onlyprint && onlyparse then error "A notation cannot be both 'only printing' and 'only parsing'.";
+ if onlyprint && onlyparse then user_err (str "A notation cannot be both 'only printing' and 'only parsing'.");
let assoc = Option.append mods.assoc (Some NonA) in
let toks = split_notation_string df in
let recvars,mainvars,symbols = analyze_notation_tokens toks in
@@ -1385,7 +1385,7 @@ let set_notation_for_interpretation impls ((_,df),c,sc) =
(try ignore
(silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false None) ());
with NoSyntaxRule ->
- error "Parsing rule for this notation has to be previously declared.");
+ user_err Pp.(str "Parsing rule for this notation has to be previously declared."));
Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc
(* Main entry point *)
diff --git a/vernac/record.ml b/vernac/record.ml
index 10207d0e0..5accc8e37 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -561,7 +561,7 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id
in
let isnot_class = match kind with Class false -> false | _ -> true in
if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then
- error "Priorities only allowed for type class substructures";
+ user_err Pp.(str "Priorities only allowed for type class substructures");
(* Now, younger decl in params and fields is on top *)
let (pl, ctx), arity, template, implpars, params, implfs, fields =
States.with_state_protection (fun () ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index a08c79c40..6c1d64cfe 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -139,7 +139,7 @@ let make_cases s =
let show_match id =
let patterns =
try make_cases_aux (Nametab.global id)
- with Not_found -> error "Unknown inductive type."
+ with Not_found -> user_err Pp.(str "Unknown inductive type.")
in
let pr_branch l =
str "| " ++ hov 1 (prlist_with_sep spc str l) ++ str " =>"
@@ -305,7 +305,7 @@ let print_strategy r =
let key = match r with
| VarRef id -> VarKey id
| ConstRef cst -> ConstKey cst
- | IndRef _ | ConstructRef _ -> error "The reference is not unfoldable"
+ | IndRef _ | ConstructRef _ -> user_err Pp.(str "The reference is not unfoldable")
in
let lvl = get_strategy oracle key in
Feedback.msg_notice (pr_strategy (r, lvl))
@@ -451,8 +451,8 @@ let start_proof_and_print k l hook =
concl (Tacticals.New.tclCOMPLETE tac)
in Evd.set_universe_context sigma ctx, EConstr.of_constr c
with Logic_monad.TacticFailure e when Logic.catchable_exception e ->
- error "The statement obligations could not be resolved \
- automatically, write a statement definition first."
+ user_err Pp.(str "The statement obligations could not be resolved \
+ automatically, write a statement definition first.")
in Some hook
else None
in
@@ -551,9 +551,9 @@ let vernac_inductive poly lo finite indl =
indl;
match indl with
| [ ( _ , _ , _ ,(Record|Structure), Constructors _ ),_ ] ->
- CErrors.error "The Record keyword is for types defined using the syntax { ... }."
+ user_err Pp.(str "The Record keyword is for types defined using the syntax { ... }.")
| [ (_ , _ , _ ,Variant, RecordDecl _),_ ] ->
- CErrors.error "The Variant keyword does not support syntax { ... }."
+ user_err Pp.(str "The Variant keyword does not support syntax { ... }.")
| [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] ->
vernac_record (match b with Class _ -> Class false | _ -> b)
poly finite id bl c oc fs
@@ -564,16 +564,16 @@ let vernac_inductive poly lo finite indl =
(((coe', AssumExpr ((loc, Name id), ce)), None), [])
in vernac_record (Class true) poly finite id bl c None [f]
| [ ( _ , _, _, Class _, Constructors _), [] ] ->
- CErrors.error "Inductive classes not supported"
+ user_err Pp.(str "Inductive classes not supported")
| [ ( id , bl , c , Class _, _), _ :: _ ] ->
- CErrors.error "where clause not supported for classes"
+ user_err Pp.(str "where clause not supported for classes")
| [ ( _ , _ , _ , _, RecordDecl _ ) , _ ] ->
- CErrors.error "where clause not supported for (co)inductive records"
+ user_err Pp.(str "where clause not supported for (co)inductive records")
| _ -> let unpack = function
| ( (false, id) , bl , c , _ , Constructors l ) , ntn -> ( id , bl , c , l ) , ntn
| ( (true,_),_,_,_,Constructors _),_ ->
- CErrors.error "Variant types do not handle the \"> Name\" syntax, which is reserved for records. Use the \":>\" syntax on constructors instead."
- | _ -> CErrors.error "Cannot handle mutually (co)inductive records."
+ user_err Pp.(str "Variant types do not handle the \"> Name\" syntax, which is reserved for records. Use the \":>\" syntax on constructors instead.")
+ | _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.")
in
let indl = List.map unpack indl in
do_mutual_inductive indl poly lo finite
@@ -631,11 +631,11 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast =
(* We check the state of the system (in section, in module type)
and what module information is supplied *)
if Lib.sections_are_opened () then
- error "Modules and Module Types are not allowed inside sections.";
+ user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
let binders_ast = List.map
(fun (export,idl,ty) ->
if not (Option.is_empty export) then
- error "Arguments of a functor declaration cannot be exported. Remove the \"Export\" and \"Import\" keywords from every functor argument."
+ user_err Pp.(str "Arguments of a functor declaration cannot be exported. Remove the \"Export\" and \"Import\" keywords from every functor argument.")
else (idl,ty)) binders_ast in
let mp =
Declaremods.declare_module Modintern.interp_module_ast
@@ -649,7 +649,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
(* We check the state of the system (in section, in module type)
and what module information is supplied *)
if Lib.sections_are_opened () then
- error "Modules and Module Types are not allowed inside sections.";
+ user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
match mexpr_ast_l with
| [] ->
check_no_pending_proofs ();
@@ -674,7 +674,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
let binders_ast = List.map
(fun (export,idl,ty) ->
if not (Option.is_empty export) then
- error "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument."
+ user_err Pp.(str "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument.")
else (idl,ty)) binders_ast in
let mp =
Declaremods.declare_module Modintern.interp_module_ast
@@ -694,7 +694,7 @@ let vernac_end_module export (loc,id as lid) =
let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
if Lib.sections_are_opened () then
- error "Modules and Module Types are not allowed inside sections.";
+ user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
match mty_ast_l with
| [] ->
@@ -722,7 +722,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
let binders_ast = List.map
(fun (export,idl,ty) ->
if not (Option.is_empty export) then
- error "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument."
+ user_err Pp.(str "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument.")
else (idl,ty)) binders_ast in
let mp =
Declaremods.declare_modtype Modintern.interp_module_ast
@@ -846,7 +846,7 @@ let vernac_set_end_tac tac =
let env = Genintern.empty_glob_sign (Global.env ()) in
let _, tac = Genintern.generic_intern env tac in
if not (refining ()) then
- error "Unknown command of the non proof-editing mode.";
+ user_err Pp.(str "Unknown command of the non proof-editing mode.");
set_end_tac tac
(* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
@@ -903,7 +903,7 @@ let vernac_chdir = function
(* Cd is typically used to control the output directory of
extraction. A failed Cd could lead to overwriting .ml files
so we make it an error. *)
- CErrors.error ("Cd failed: " ^ err)
+ user_err Pp.(str ("Cd failed: " ^ err))
end;
if_verbose Feedback.msg_info (str (Sys.getcwd()))
@@ -972,7 +972,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
let never_unfold_flag = List.mem `ReductionNeverUnfold flags in
let err_incompat x y =
- error ("Options \""^x^"\" and \""^y^"\" are incompatible.") in
+ user_err Pp.(str ("Options \""^x^"\" and \""^y^"\" are incompatible.")) in
if assert_flag && rename_flag then
err_incompat "assert" "rename";
@@ -1018,7 +1018,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
| { name = Anonymous; notation_scope = Some _ } :: args ->
check_extra_args args
| _ ->
- error "Extra notation scopes can be set on anonymous and explicit arguments only."
+ user_err Pp.(str "Extra notation scopes can be set on anonymous and explicit arguments only.")
in
let args, scopes =
@@ -1032,12 +1032,12 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
in
if Option.cata (fun n -> n > num_args) false nargs_for_red then
- error "The \"/\" modifier should be put before any extra scope.";
+ user_err Pp.(str "The \"/\" modifier should be put before any extra scope.");
let scopes_specified = List.exists Option.has_some scopes in
if scopes_specified && clear_scopes_flag then
- error "The \"clear scopes\" flag is incompatible with scope annotations.";
+ user_err Pp.(str "The \"clear scopes\" flag is incompatible with scope annotations.");
let names = List.map (fun { name } -> name) args in
let names = names :: List.map (List.map fst) more_implicits in
@@ -1062,7 +1062,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
| name1 :: names1, name2 :: names2 ->
if Name.equal name1 name2 then
name1 :: names_union names1 names2
- else error "Argument lists should agree on the names they provide."
+ else user_err Pp.(str "Argument lists should agree on the names they provide.")
in
let names = List.fold_left names_union [] names in
@@ -1143,10 +1143,10 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
let implicits_specified = match implicits with [[]] -> false | _ -> true in
if implicits_specified && clear_implicits_flag then
- error "The \"clear implicits\" flag is incompatible with implicit annotations";
+ user_err Pp.(str "The \"clear implicits\" flag is incompatible with implicit annotations");
if implicits_specified && default_implicits_flag then
- error "The \"default implicits\" flag is incompatible with implicit annotations";
+ user_err Pp.(str "The \"default implicits\" flag is incompatible with implicit annotations");
let rargs =
Util.List.map_filter (function (n, true) -> Some n | _ -> None)
@@ -1452,8 +1452,8 @@ let vernac_set_strategy locality l =
match smart_global r with
| ConstRef sp -> EvalConstRef sp
| VarRef id -> EvalVarRef id
- | _ -> error
- "cannot set an inductive type or a constructor as transparent" in
+ | _ -> user_err Pp.(str
+ "cannot set an inductive type or a constructor as transparent") in
let l = List.map (fun (lev,ql) -> (lev,List.map glob_ref ql)) l in
Redexpr.set_strategy local l
@@ -1463,8 +1463,8 @@ let vernac_set_opacity locality (v,l) =
match smart_global r with
| ConstRef sp -> EvalConstRef sp
| VarRef id -> EvalVarRef id
- | _ -> error
- "cannot set an inductive type or a constructor as transparent" in
+ | _ -> user_err Pp.(str
+ "cannot set an inductive type or a constructor as transparent") in
let l = List.map glob_ref l in
Redexpr.set_strategy local [v,l]
@@ -1764,10 +1764,10 @@ let vernac_locate = let open Feedback in function
let vernac_register id r =
if Pfedit.refining () then
- error "Cannot register a primitive while in proof editing mode.";
+ user_err Pp.(str "Cannot register a primitive while in proof editing mode.");
let t = (Constrintern.global_reference (snd id)) in
if not (isConst t) then
- error "Register inline: a constant is expected";
+ user_err Pp.(str "Register inline: a constant is expected");
let kn = destConst t in
match r with
| RegisterInline -> Global.register_inline (Univ.out_punivs kn)
@@ -1780,7 +1780,7 @@ let vernac_focus gln =
match gln with
| None -> Proof.focus focus_command_cond () 1 p
| Some 0 ->
- CErrors.error "Invalid goal number: 0. Goal numbering starts with 1."
+ user_err Pp.(str "Invalid goal number: 0. Goal numbering starts with 1.")
| Some n ->
Proof.focus focus_command_cond () n p)
@@ -1795,7 +1795,7 @@ let vernac_unfocused () =
if Proof.unfocused p then
Feedback.msg_notice (str"The proof is indeed fully unfocused.")
else
- error "The proof is not fully unfocused."
+ user_err Pp.(str "The proof is not fully unfocused.")
(* BeginSubproof / EndSubproof.
@@ -2081,7 +2081,7 @@ let check_vernac_supports_locality c l =
| VernacDeclareReduction _
| VernacExtend _
| VernacInductive _) -> ()
- | Some _, _ -> CErrors.error "This command does not support Locality"
+ | Some _, _ -> user_err Pp.(str "This command does not support Locality")
(* Vernaculars that take a polymorphism flag *)
let check_vernac_supports_polymorphism c p =
@@ -2095,7 +2095,7 @@ let check_vernac_supports_polymorphism c p =
| VernacInstance _ | VernacDeclareInstances _
| VernacHints _ | VernacContext _
| VernacExtend _ | VernacUniverse _ | VernacConstraint _) -> ()
- | Some _, _ -> CErrors.error "This command does not support Polymorphism"
+ | Some _, _ -> user_err Pp.(str "This command does not support Polymorphism")
let enforce_polymorphism = function
| None -> Flags.is_universe_polymorphism ()
@@ -2172,13 +2172,13 @@ let interp ?(verbosely=true) ?proof (loc,c) =
| VernacStm _ -> assert false (* Done by Stm *)
| VernacProgram c when not isprogcmd -> aux ?locality ?polymorphism true c
- | VernacProgram _ -> CErrors.error "Program mode specified twice"
+ | VernacProgram _ -> user_err Pp.(str "Program mode specified twice")
| VernacLocal (b, c) when Option.is_empty locality ->
aux ~locality:b ?polymorphism isprogcmd c
| VernacPolymorphic (b, c) when polymorphism = None ->
aux ?locality ~polymorphism:b isprogcmd c
- | VernacPolymorphic (b, c) -> CErrors.error "Polymorphism specified twice"
- | VernacLocal _ -> CErrors.error "Locality specified twice"
+ | VernacPolymorphic (b, c) -> user_err Pp.(str "Polymorphism specified twice")
+ | VernacLocal _ -> user_err Pp.(str "Locality specified twice")
| VernacFail v ->
with_fail true (fun () -> aux ?locality ?polymorphism isprogcmd v)
| VernacTimeout (n,v) ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 15:53:32 +0000