aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/classes.ml6
-rw-r--r--vernac/command.ml16
-rw-r--r--vernac/explainErr.ml5
-rw-r--r--vernac/lemmas.ml4
-rw-r--r--vernac/metasyntax.ml2
-rw-r--r--vernac/obligations.ml4
-rw-r--r--vernac/record.ml8
-rw-r--r--vernac/topfmt.ml2
-rw-r--r--vernac/vernacentries.ml96
9 files changed, 72 insertions, 71 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml
index bdaa3ece6..fb300dbc1 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -77,7 +77,7 @@ let existing_instance glob g info =
match class_of_constr Evd.empty (EConstr.of_constr r) with
| Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob
(*FIXME*) (Flags.use_polymorphic_flag ()) c)
- | None -> user_err ~loc:(loc_of_reference g)
+ | None -> user_err ?loc:(loc_of_reference g)
~hdr:"declare_instance"
(Pp.str "Constant does not build instances of a declared type class.")
@@ -237,7 +237,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
let get_id =
function
| Ident id' -> id'
- | Qualid (loc,id') -> (loc, snd (repr_qualid id'))
+ | Qualid (loc,id') -> (Loc.tag ?loc @@ snd (repr_qualid id'))
in
let props, rest =
List.fold_left
@@ -257,7 +257,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
let (loc, mid) = get_id loc_mid in
List.iter (fun (n, _, x) ->
if Name.equal n (Name mid) then
- Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) x)
+ Option.iter (fun x -> Dumpglob.add_glob ?loc (ConstRef x)) x)
k.cl_projs;
c :: props, rest'
with Not_found ->
diff --git a/vernac/command.ml b/vernac/command.ml
index fbaa09430..82d7b19d7 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -53,16 +53,16 @@ let rec under_binders env sigma f n c =
mkLetIn (x,b,t,under_binders (push_rel (LocalDef (x,b,t)) env) sigma f (n-1) c)
| _ -> assert false
-let rec complete_conclusion a cs = Loc.map_with_loc (fun ~loc -> function
+let rec complete_conclusion a cs = Loc.map_with_loc (fun ?loc -> function
| CProdN (bl,c) -> CProdN (bl,complete_conclusion a cs c)
| CLetIn (na,b,t,c) -> CLetIn (na,b,t,complete_conclusion a cs c)
| CHole (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 -> Loc.tag ~loc @@ CRef(Ident(loc,id),None)) params in
+ let args = List.map (fun id -> Loc.tag ?loc @@ CRef(Ident(loc,id),None)) params in
CAppExpl ((None,Ident(loc,name),None),List.rev args)
| c -> c
)
@@ -344,7 +344,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
@@ -356,7 +356,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
@@ -452,7 +452,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 (Reductionops.is_arity env !evdref 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
let t = EConstr.Unsafe.to_constr t in
t, pseudo_poly, impls
@@ -566,7 +566,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
@@ -982,7 +982,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let relty = Typing.unsafe_type_of env !evdref rel in
let relargty =
let error () =
- user_err ~loc:(constr_loc r)
+ user_err ?loc:(constr_loc r)
~hdr:"Command.build_wellfounded"
(Printer.pr_econstr_env env !evdref rel ++ str " is not an homogeneous binary relation.")
in
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index ed2dd274a..040c86805 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -117,8 +117,9 @@ let process_vernac_interp_error ?(allow_uncaught=true) (exc, info) =
try Some (CList.find_map (fun f -> f e) !additional_error_info)
with _ -> None
in
+ let add_loc_opt ?loc info = Option.cata (fun l -> Loc.add_loc info l) info loc in
match e' with
| None -> e
- | Some (loc, None) -> (fst e, Loc.add_loc (snd e) loc)
+ | Some (loc, None) -> (fst e, add_loc_opt ?loc (snd e))
| Some (loc, Some msg) ->
- (EvaluatedError (msg, Some (fst e)), Loc.add_loc (snd e) loc)
+ (EvaluatedError (msg, Some (fst e)), add_loc_opt ?loc (snd e))
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index b51792b1e..c6f9f21d8 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -224,7 +224,7 @@ let compute_proof_name locality = function
if Nametab.exists_cci (Lib.make_path id) || is_section_variable id ||
locality == Global && Nametab.exists_cci (Lib.make_path_except_section id)
then
- user_err ~loc (pr_id id ++ str " already exists.");
+ user_err ?loc (pr_id id ++ str " already exists.");
id, pl
| None ->
next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()), None
@@ -337,7 +337,7 @@ let get_proof proof do_guard hook opacity =
let check_exist =
List.iter (fun (loc,id) ->
if not (Nametab.exists_cci (Lib.make_path id)) then
- user_err ~loc (pr_id id ++ str " does not exist.")
+ user_err ?loc (pr_id id ++ str " does not exist.")
)
let universe_proof_terminator compute_guard hook =
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index a586fe9f2..feacfe915 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -192,7 +192,7 @@ let parse_format ((loc, str) : lstring) =
error "Empty format."
with reraise ->
let (e, info) = CErrors.push reraise in
- let info = Loc.add_loc info loc in
+ let info = Option.cata (Loc.add_loc info) info loc in
iraise (e, info)
(***********************)
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 5e65855ef..f0883e286 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -38,7 +38,7 @@ let check_evars env evm =
| Evar_kinds.QuestionMark _
| Evar_kinds.ImplicitArg (_,_,false) -> ()
| _ ->
- Pretype_errors.error_unsolvable_implicit ~loc env evm key None)
+ Pretype_errors.error_unsolvable_implicit ?loc env evm key None)
(Evd.undefined_map evm)
type oblinfo =
@@ -991,7 +991,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) ~hdr:"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/vernac/record.ml b/vernac/record.ml
index 95f5ad7cc..8bd583b81 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -94,7 +94,7 @@ let compute_constructor_level evars env l =
let binder_of_decl = function
| Vernacexpr.AssumExpr(n,t) -> (n,None,t)
| Vernacexpr.DefExpr(n,c,t) -> (n,Some c, match t with Some c -> c
- | None -> Loc.tag ~loc:(fst n) @@ CHole (None, Misctypes.IntroAnonymous, None))
+ | None -> Loc.tag ?loc:(fst n) @@ CHole (None, Misctypes.IntroAnonymous, None))
let binders_of_decls = List.map binder_of_decl
@@ -106,14 +106,14 @@ 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 ~hdr:"record" (str "Record parameters must be named")
+ user_err ?loc ~hdr:"record" (str "Record parameters must be named")
| _ -> ()
in
List.iter
(function CLocalDef (b, _, _) -> error default_binder_kind b
| CLocalAssum (ls, bk, ce) -> List.iter (error bk) ls
| CLocalPattern (loc,(_,_)) ->
- Loc.raise ~loc (Stream.Error "pattern with quote not allowed in record parameters.")) ps
+ Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters.")) ps
in
let impls_env, ((env1,newps), imps) = interp_context_evars env0 evars ps in
let newps = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) newps in
@@ -135,7 +135,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
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index c25dd55fb..2f01cfb54 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -108,7 +108,7 @@ end
type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit
-let msgnl_with ?pre_hdr fmt strm =
+let msgnl_with fmt strm =
pp_with fmt (strm ++ fnl ());
Format.pp_print_flush fmt ()
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 75f403e33..a78350749 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -364,43 +364,43 @@ let msg_found_library = function
Feedback.msg_info (hov 0
(pr_dirpath fulldir ++ strbrk " is bound to file " ++ str file))
-let err_unmapped_library loc ?from qid =
+let err_unmapped_library ?loc ?from qid =
let dir = fst (repr_qualid qid) in
let prefix = match from with
| None -> str "."
| Some from ->
str " and prefix " ++ pr_dirpath from ++ str "."
in
- user_err ~loc
+ user_err ?loc
~hdr:"locate_library"
(strbrk "Cannot find a physical path bound to logical path matching suffix " ++
pr_dirpath dir ++ prefix)
-let err_notfound_library loc ?from qid =
+let err_notfound_library ?loc ?from qid =
let prefix = match from with
| None -> str "."
| Some from ->
str " with prefix " ++ pr_dirpath from ++ str "."
in
- user_err ~loc ~hdr:"locate_library"
+ user_err ?loc ~hdr:"locate_library"
(strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix)
let print_located_library r =
let (loc,qid) = qualid_of_reference r in
try msg_found_library (Library.locate_qualified_library ~warn:false qid)
with
- | Library.LibUnmappedDir -> err_unmapped_library loc qid
- | Library.LibNotFound -> err_notfound_library loc qid
+ | Library.LibUnmappedDir -> err_unmapped_library ?loc qid
+ | Library.LibNotFound -> err_notfound_library ?loc qid
let smart_global r =
let gr = Smartlocate.smart_global r in
- Dumpglob.add_glob (Stdarg.loc_of_or_by_notation loc_of_reference r) gr;
+ Dumpglob.add_glob ?loc:(Stdarg.loc_of_or_by_notation loc_of_reference r) gr;
gr
let dump_global r =
try
let gr = Smartlocate.smart_global r in
- Dumpglob.add_glob (Stdarg.loc_of_or_by_notation loc_of_reference r) gr
+ Dumpglob.add_glob ?loc:(Stdarg.loc_of_or_by_notation loc_of_reference r) gr
with e when CErrors.noncritical e -> ()
(**********)
(* Syntax *)
@@ -608,14 +608,14 @@ let vernac_combined_scheme lid l =
let vernac_universe loc poly l =
if poly && not (Lib.sections_are_opened ()) then
- user_err ~loc ~hdr:"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 ~hdr:"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
@@ -641,7 +641,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast =
Declaremods.declare_module Modintern.interp_module_ast
id binders_ast (Enforce mty_ast) []
in
- Dumpglob.dump_moddef loc mp "mod";
+ Dumpglob.dump_moddef ?loc mp "mod";
if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is declared");
Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)]) export
@@ -662,7 +662,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
Declaremods.start_module Modintern.interp_module_ast
export id binders_ast mty_ast_o
in
- Dumpglob.dump_moddef loc mp "mod";
+ Dumpglob.dump_moddef ?loc mp "mod";
if_verbose Feedback.msg_info
(str "Interactive Module " ++ pr_id id ++ str " started");
List.iter
@@ -680,7 +680,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
Declaremods.declare_module Modintern.interp_module_ast
id binders_ast mty_ast_o mexpr_ast_l
in
- Dumpglob.dump_moddef loc mp "mod";
+ Dumpglob.dump_moddef ?loc mp "mod";
if_verbose Feedback.msg_info
(str "Module " ++ pr_id id ++ str " is defined");
Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)])
@@ -688,7 +688,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
let vernac_end_module export (loc,id as lid) =
let mp = Declaremods.end_module () in
- Dumpglob.dump_modref loc mp "mod";
+ Dumpglob.dump_modref ?loc mp "mod";
if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is defined");
Option.iter (fun export -> vernac_import export [Ident lid]) export
@@ -709,7 +709,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
Declaremods.start_modtype Modintern.interp_module_ast
id binders_ast mty_sign
in
- Dumpglob.dump_moddef loc mp "modtype";
+ Dumpglob.dump_moddef ?loc mp "modtype";
if_verbose Feedback.msg_info
(str "Interactive Module Type " ++ pr_id id ++ str " started");
List.iter
@@ -728,13 +728,13 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
Declaremods.declare_modtype Modintern.interp_module_ast
id binders_ast mty_sign mty_ast_l
in
- Dumpglob.dump_moddef loc mp "modtype";
+ Dumpglob.dump_moddef ?loc mp "modtype";
if_verbose Feedback.msg_info
(str "Module Type " ++ pr_id id ++ str " is defined")
let vernac_end_modtype (loc,id) =
let mp = Declaremods.end_modtype () in
- Dumpglob.dump_modref loc mp "modtype";
+ Dumpglob.dump_modref ?loc mp "modtype";
if_verbose Feedback.msg_info (str "Module Type " ++ pr_id id ++ str " is defined")
let vernac_include l =
@@ -751,7 +751,7 @@ let vernac_begin_section (_, id as lid) =
Lib.open_section id
let vernac_end_section (loc,_) =
- Dumpglob.dump_reference loc
+ Dumpglob.dump_reference ?loc
(DirPath.to_string (Lib.current_dirpath true)) "<>" "sec";
Lib.close_section ()
@@ -784,12 +784,12 @@ let vernac_require from import qidl =
let (_, dir, f) = Library.locate_qualified_library ?root ~warn qid in
(dir, f)
with
- | Library.LibUnmappedDir -> err_unmapped_library loc ?from:root qid
- | Library.LibNotFound -> err_notfound_library loc ?from:root qid
+ | Library.LibUnmappedDir -> err_unmapped_library ?loc ?from:root qid
+ | Library.LibNotFound -> err_notfound_library ?loc ?from:root qid
in
let modrefl = List.map locate qidl in
if Dumpglob.dump () then
- List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl (List.map fst modrefl);
+ List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref ?loc dp "lib") qidl (List.map fst modrefl);
Library.require_library_from_dirpath modrefl import
(* Coercions and canonical structures *)
@@ -1179,7 +1179,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
let scopes = List.map (Option.map (fun (loc,k) ->
try ignore (Notation.find_scope k); k
with UserError _ ->
- Notation.find_delimiters_scope ~loc k)) scopes
+ Notation.find_delimiters_scope ?loc k)) scopes
in
vernac_arguments_scope locality reference scopes
end;
@@ -1533,14 +1533,14 @@ let get_current_context_of_args = function
| Some n -> get_goal_context n
| None -> get_current_context ()
-let query_command_selector ~loc = function
+let query_command_selector ?loc = function
| None -> None
| Some (SelectNth n) -> Some n
- | _ -> user_err ~loc ~hdr:"query_command_selector"
+ | _ -> user_err ?loc ~hdr:"query_command_selector"
(str "Query commands only support the single numbered goal selector.")
-let vernac_check_may_eval ~loc redexp glopt rc =
- let glopt = query_command_selector ~loc glopt in
+let vernac_check_may_eval ?loc redexp glopt rc =
+ let glopt = query_command_selector ?loc glopt in
let (sigma, env) = get_current_context_of_args glopt in
let sigma', c = interp_open_constr env sigma rc in
let c = EConstr.Unsafe.to_constr c in
@@ -1602,10 +1602,10 @@ exception NoHyp
(* Printing "About" information of a hypothesis of the current goal.
We only print the type and a small statement to this comes from the
goal. Precondition: there must be at least one current goal. *)
-let print_about_hyp_globs ~loc ref_or_by_not glopt =
+let print_about_hyp_globs ?loc ref_or_by_not glopt =
let open Context.Named.Declaration in
try
- let glnumopt = query_command_selector ~loc glopt in
+ let glnumopt = query_command_selector ?loc glopt in
let gl,id =
match glnumopt,ref_or_by_not with
| None,AN (Ident (_loc,id)) -> (* goal number not given, catch any failure *)
@@ -1613,7 +1613,7 @@ let print_about_hyp_globs ~loc ref_or_by_not glopt =
| Some n,AN (Ident (_loc,id)) -> (* goal number given, catch if wong *)
(try get_nth_goal n,id
with
- Failure _ -> user_err ~loc ~hdr:"print_about_hyp_globs"
+ Failure _ -> user_err ?loc ~hdr:"print_about_hyp_globs"
(str "No such goal: " ++ int n ++ str "."))
| _ , _ -> raise NoHyp in
let hyps = pf_hyps gl in
@@ -1627,7 +1627,7 @@ let print_about_hyp_globs ~loc ref_or_by_not glopt =
| NoHyp | Not_found -> print_about ref_or_by_not
-let vernac_print ~loc = let open Feedback in function
+let vernac_print ?loc = let open Feedback in function
| PrintTables -> msg_notice (print_tables ())
| PrintFullContext-> msg_notice (print_full_context_typ ())
| PrintSectionContext qid -> msg_notice (print_sec_context_typ qid)
@@ -1672,7 +1672,7 @@ let vernac_print ~loc = let open Feedback in function
| PrintVisibility s ->
msg_notice (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s)
| PrintAbout (ref_or_by_not,glnumopt) ->
- msg_notice (print_about_hyp_globs ~loc ref_or_by_not glnumopt)
+ msg_notice (print_about_hyp_globs ?loc ref_or_by_not glnumopt)
| PrintImplicit qid ->
dump_global qid; msg_notice (print_impargs qid)
| PrintAssumptions (o,t,r) ->
@@ -1689,7 +1689,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 ~hdr:"global_module"
+ user_err ?loc ~hdr:"global_module"
(str "Module/section " ++ pr_qualid qid ++ str " not found.")
let interp_search_restriction = function
@@ -1737,8 +1737,8 @@ let _ =
optread = (fun () -> !search_output_name_only);
optwrite = (:=) search_output_name_only }
-let vernac_search ~loc s gopt r =
- let gopt = query_command_selector ~loc gopt in
+let vernac_search ?loc s gopt r =
+ let gopt = query_command_selector ?loc gopt in
let r = interp_search_restriction r in
let env,gopt =
match gopt with | None ->
@@ -1913,7 +1913,7 @@ let vernac_load interp fname =
* is the outdated/deprecated "Local" attribute of some vernacular commands
* still parsed as the obsolete_locality grammar entry for retrocompatibility.
* loc is the Loc.t of the vernacular command being interpreted. *)
-let interp ?proof ~loc locality poly c =
+let interp ?proof ?loc locality poly c =
vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac c);
match c with
(* The below vernac are candidates for removal from the main type
@@ -2045,11 +2045,11 @@ let interp ?proof ~loc locality poly c =
| VernacAddOption (key,v) -> vernac_add_option key v
| VernacMemOption (key,v) -> vernac_mem_option key v
| VernacPrintOption key -> vernac_print_option key
- | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval ~loc r g c
+ | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval ?loc r g c
| VernacDeclareReduction (s,r) -> vernac_declare_reduction locality s r
| VernacGlobalCheck c -> vernac_global_check c
- | VernacPrint p -> vernac_print ~loc p
- | VernacSearch (s,g,r) -> vernac_search ~loc s g r
+ | VernacPrint p -> vernac_print ?loc p
+ | VernacSearch (s,g,r) -> vernac_search ?loc s g r
| VernacLocate l -> vernac_locate l
| VernacRegister (id, r) -> vernac_register id r
| VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n")
@@ -2065,15 +2065,15 @@ let interp ?proof ~loc locality poly c =
| VernacShow s -> vernac_show s
| VernacCheckGuard -> vernac_check_guard ()
| VernacProof (None, None) ->
- Aux_file.record_in_aux_at ~loc "VernacProof" "tac:no using:no"
+ Aux_file.record_in_aux_at ?loc "VernacProof" "tac:no using:no"
| VernacProof (Some tac, None) ->
- Aux_file.record_in_aux_at ~loc "VernacProof" "tac:yes using:no";
+ Aux_file.record_in_aux_at ?loc "VernacProof" "tac:yes using:no";
vernac_set_end_tac tac
| VernacProof (None, Some l) ->
- Aux_file.record_in_aux_at ~loc "VernacProof" "tac:no using:yes";
+ Aux_file.record_in_aux_at ?loc "VernacProof" "tac:no using:yes";
vernac_set_used_variables l
| VernacProof (Some tac, Some l) ->
- Aux_file.record_in_aux_at ~loc "VernacProof" "tac:yes using:yes";
+ Aux_file.record_in_aux_at ?loc "VernacProof" "tac:yes using:yes";
vernac_set_end_tac tac; vernac_set_used_variables l
| VernacProofMode mn -> Proof_global.set_proof_mode mn
@@ -2149,10 +2149,10 @@ let vernac_timeout f =
let restore_timeout () = current_timeout := None
-let locate_if_not_already loc (e, info) =
+let locate_if_not_already ?loc (e, info) =
match Loc.get_loc info with
- | None -> (e, Loc.add_loc info loc)
- | Some l -> if Loc.is_ghost l then (e, Loc.add_loc info loc) else (e, info)
+ | None -> (e, Option.cata (Loc.add_loc info) info loc)
+ | Some l -> (e, info)
exception HasNotFailed
exception HasFailed of std_ppcmds
@@ -2219,8 +2219,8 @@ let interp ?(verbosely=true) ?proof (loc,c) =
try
vernac_timeout begin fun () ->
if verbosely
- then Flags.verbosely (interp ?proof ~loc locality poly) c
- else Flags.silently (interp ?proof ~loc locality poly) c;
+ then Flags.verbosely (interp ?proof ?loc locality poly) c
+ else Flags.silently (interp ?proof ?loc locality poly) c;
if orig_program_mode || not !Flags.program_mode || isprogcmd then
Flags.program_mode := orig_program_mode;
ignore (Flags.use_polymorphic_flag ())
@@ -2232,7 +2232,7 @@ let interp ?(verbosely=true) ?proof (loc,c) =
| e -> CErrors.noncritical e)
->
let e = CErrors.push reraise in
- let e = locate_if_not_already loc e in
+ let e = locate_if_not_already ?loc e in
let () = restore_timeout () in
Flags.program_mode := orig_program_mode;
ignore (Flags.use_polymorphic_flag ());
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 15:46:17 +0000