diff options
Diffstat (limited to 'vernac')
-rw-r--r-- | vernac/classes.ml | 6 | ||||
-rw-r--r-- | vernac/command.ml | 16 | ||||
-rw-r--r-- | vernac/explainErr.ml | 5 | ||||
-rw-r--r-- | vernac/lemmas.ml | 4 | ||||
-rw-r--r-- | vernac/metasyntax.ml | 2 | ||||
-rw-r--r-- | vernac/obligations.ml | 4 | ||||
-rw-r--r-- | vernac/record.ml | 8 | ||||
-rw-r--r-- | vernac/topfmt.ml | 2 | ||||
-rw-r--r-- | vernac/vernacentries.ml | 96 |
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 ()); |