aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/auto_ind_decl.ml12
-rw-r--r--vernac/classes.ml16
-rw-r--r--vernac/command.ml54
-rw-r--r--vernac/explainErr.ml7
-rw-r--r--vernac/explainErr.mli2
-rw-r--r--vernac/indschemes.ml2
-rw-r--r--vernac/lemmas.ml17
-rw-r--r--vernac/metasyntax.ml6
-rw-r--r--vernac/obligations.ml9
-rw-r--r--vernac/record.ml13
-rw-r--r--vernac/topfmt.ml4
-rw-r--r--vernac/vernacentries.ml112
-rw-r--r--vernac/vernacentries.mli2
13 files changed, 122 insertions, 134 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index f363deac6..31d610abd 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -57,8 +57,6 @@ exception NonSingletonProp of inductive
exception DecidabilityMutualNotSupported
exception NoDecidabilityCoInductive
-let dl = Loc.ghost
-
let constr_of_global g = lazy (Universes.constr_of_global g)
(* Some pre declaration of constant we are going to use *)
@@ -85,12 +83,12 @@ let destruct_on c = destruct false None c None None
let destruct_on_using c id =
destruct false None c
- (Some (dl,IntroOrPattern [[dl,IntroNaming IntroAnonymous];
- [dl,IntroNaming (IntroIdentifier id)]]))
+ (Some (Loc.tag @@ IntroOrPattern [[Loc.tag @@ IntroNaming IntroAnonymous];
+ [Loc.tag @@ IntroNaming (IntroIdentifier id)]]))
None
let destruct_on_as c l =
- destruct false None c (Some (dl,l)) None
+ destruct false None c (Some (Loc.tag l)) None
(* reconstruct the inductive with the correct de Bruijn indexes *)
let mkFullInd (ind,u) n =
@@ -608,8 +606,8 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
Proofview.Goal.enter { enter = begin fun gl ->
let fresht = fresh_id (Id.of_string "Z") gl in
destruct_on_as (EConstr.mkVar freshz)
- (IntroOrPattern [[dl,IntroNaming (IntroIdentifier fresht);
- dl,IntroNaming (IntroIdentifier freshz)]])
+ (IntroOrPattern [[Loc.tag @@ IntroNaming (IntroIdentifier fresht);
+ Loc.tag @@ IntroNaming (IntroIdentifier freshz)]])
end }
]);
(*
diff --git a/vernac/classes.ml b/vernac/classes.ml
index e760487bd..5843da31e 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -74,7 +74,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.")
@@ -144,14 +144,14 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
(fun avoid (clname, _) ->
match clname with
| Some (cl, b) ->
- let t = CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in
+ let t = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None) in
t, avoid
| None -> failwith ("new instance: under-applied typeclass"))
cl
| Explicit -> cl, Id.Set.empty
in
let tclass =
- if generalize then CGeneralization (Loc.ghost, Implicit, Some AbsPi, tclass)
+ if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass)
else tclass
in
let k, u, cty, ctx', ctx, len, imps, subst =
@@ -214,7 +214,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
else (
let props =
match props with
- | Some (true, CRecord (loc, fs)) ->
+ | Some (true, { CAst.v = CRecord fs }) ->
if List.length fs > List.length k.cl_props then
mismatched_props env' (List.map snd fs) k.cl_props;
Some (Inl fs)
@@ -234,7 +234,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
@@ -254,11 +254,11 @@ 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 ->
- (CHole (Loc.ghost, None(* Some Evar_kinds.GoalEvar *), Misctypes.IntroAnonymous, None) :: props), rest
+ ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Misctypes.IntroAnonymous, None)) :: props), rest
else props, rest)
([], props) k.cl_props
in
@@ -405,7 +405,7 @@ let context poly l =
let decl = (Discharge, poly, Definitional) in
let nstatus =
pi3 (Command.declare_assumption false decl (t, !uctx) [] [] impl
- Vernacexpr.NoInline (Loc.ghost, id))
+ Vernacexpr.NoInline (Loc.tag id))
in
let () = uctx := Univ.ContextSet.empty in
status && nstatus
diff --git a/vernac/command.ml b/vernac/command.ml
index 2fa2aa4e3..8a9bbb884 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -53,18 +53,19 @@ 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 = function
- | CProdN (loc,bl,c) -> CProdN (loc,bl,complete_conclusion a cs c)
- | CLetIn (loc,na,b,t,c) -> CLetIn (loc,na,b,t,complete_conclusion a cs c)
- | CHole (loc, k, _, _) ->
+let rec complete_conclusion a cs = CAst.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 -> CRef(Ident(loc,id),None)) params in
- CAppExpl (loc,(None,Ident(loc,name),None),List.rev args)
+ let args = List.map (fun id -> CAst.make ?loc @@ CRef(Ident(loc,id),None)) params in
+ CAppExpl ((None,Ident(loc,name),None),List.rev args)
| c -> c
+ )
(* Commands of the interface *)
@@ -266,7 +267,7 @@ match local with
(gr,inst,Lib.is_modtype_strict ())
let interp_assumption evdref env impls bl c =
- let c = mkCProdN (local_binders_loc bl) bl c in
+ let c = mkCProdN ?loc:(local_binders_loc bl) bl c in
let ty, impls = interp_type_evars_impls env evdref ~impls c in
let ty = EConstr.Unsafe.to_constr ty in
(ty, impls)
@@ -343,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
@@ -355,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
@@ -421,13 +422,13 @@ let prepare_param = function
let rec check_anonymous_type ind =
let open Glob_term in
- match ind with
- | GSort (_, GType []) -> true
- | GProd (_, _, _, _, e)
- | GLetIn (_, _, _, _, e)
- | GLambda (_, _, _, _, e)
- | GApp (_, e, _)
- | GCast (_, e, _) -> check_anonymous_type e
+ match ind.CAst.v with
+ | GSort (GType []) -> true
+ | GProd ( _, _, _, e)
+ | GLetIn (_, _, _, e)
+ | GLambda (_, _, _, e)
+ | GApp (e, _)
+ | GCast (e, _) -> check_anonymous_type e
| _ -> false
let make_conclusion_flexible evdref ty poly =
@@ -451,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
@@ -565,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
@@ -682,7 +683,7 @@ let extract_params indl =
let extract_inductive indl =
List.map (fun (((_,indname),pl),_,ar,lc) -> {
ind_name = indname; ind_univs = pl;
- ind_arity = Option.cata (fun x -> x) (CSort (Loc.ghost,GType [])) ar;
+ ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (GType [])) ar;
ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc
}) indl
@@ -918,7 +919,7 @@ let mkSubset name typ prop =
[| typ; mkLambda (name, typ, prop) |])
let sigT = Lazy.from_fun build_sigma_type
-let make_qref s = Qualid (Loc.ghost, qualid_of_string s)
+let make_qref s = Qualid (Loc.tag @@ qualid_of_string s)
let lt_ref = make_qref "Init.Peano.lt"
let rec telescope l =
@@ -983,7 +984,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
@@ -1060,7 +1061,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
mkApp (EConstr.of_constr (Universes.constr_of_global (delayed_force fix_sub_ref)),
[| argtyp ; wf_rel ;
Evarutil.e_new_evar env evdref
- ~src:(Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof;
+ ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof;
prop |])
in
let def = Typing.e_solve_evars env evdref def in
@@ -1210,7 +1211,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
let fixdefs = List.map Option.get fixdefs in
let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
let env = Global.env() in
- let indexes = search_guard Loc.ghost env indexes fixdecls in
+ let indexes = search_guard env indexes fixdecls in
let fiximps = List.map (fun (n,r,p) -> r) fiximps in
let vars = Universes.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
let fixdecls =
@@ -1322,8 +1323,7 @@ let do_program_recursive local p fixkind fixl ntns =
Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs)
in
let indexes =
- Pretyping.search_guard
- Loc.ghost (Global.env ()) possible_indexes fixdecls in
+ Pretyping.search_guard (Global.env ()) possible_indexes fixdecls in
List.iteri (fun i _ ->
Inductive.check_fix env
((indexes,i),fixdecls))
@@ -1350,7 +1350,7 @@ let do_program_fixpoint local poly l =
| [(n, CMeasureRec (m, r))], [((((_,id),pl),_,bl,typ,def),ntn)] ->
build_wellfounded (id, pl, n, bl, typ, out_def def) poly
- (Option.default (CRef (lt_ref,None)) r) m ntn
+ (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m ntn
| _, _ when List.for_all (fun (n, ro) -> ro == CStructRec) g ->
let fixl,ntns = extract_fixpoint_components true l in
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 04841c922..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 (None, loc) -> (fst e, Loc.add_loc (snd e) loc)
- | Some (Some msg, loc) ->
- (EvaluatedError (msg, Some (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)), add_loc_opt ?loc (snd e))
diff --git a/vernac/explainErr.mli b/vernac/explainErr.mli
index 370ad7e3b..9202729ce 100644
--- a/vernac/explainErr.mli
+++ b/vernac/explainErr.mli
@@ -18,4 +18,4 @@ val process_vernac_interp_error : ?allow_uncaught:bool -> Util.iexn -> Util.iexn
val explain_exn_default : exn -> Pp.std_ppcmds
-val register_additional_error_info : (Util.iexn -> (Pp.std_ppcmds option * Loc.t) option) -> unit
+val register_additional_error_info : (Util.iexn -> (Pp.std_ppcmds option Loc.located) option) -> unit
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 2458c5131..b21e80bef 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -371,7 +371,7 @@ requested
| InType -> recs ^ "t_nodep")
) in
let newid = add_suffix (basename_of_global (IndRef ind)) suffix in
- let newref = (Loc.ghost,newid) in
+ let newref = Loc.tag newid in
((newref,isdep,ind,z)::l1),l2
in
match t with
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 816cb2478..c67a3302f 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -79,7 +79,7 @@ let adjust_guardness_conditions const = function
List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l)
env (Safe_typing.side_effects_of_private_constants eff) in
let indexes =
- search_guard Loc.ghost env
+ search_guard env
possible_indexes fixdecls in
(mkFix ((indexes,0),fixdecls), ctx), eff
| _ -> (body, ctx), eff) }
@@ -206,7 +206,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
@@ -280,13 +280,6 @@ let save_anonymous ?export_seff proof save_ident =
check_anonymity id save_ident;
save ?export_seff save_ident const cstrs pl do_guard persistence hook
-let save_anonymous_with_strength ?export_seff proof kind save_ident =
- let id,const,(cstrs,pl),do_guard,_,hook = proof in
- check_anonymity id save_ident;
- (* we consider that non opaque behaves as local for discharge *)
- save ?export_seff save_ident const cstrs pl do_guard
- (Global, const.const_entry_polymorphic, Proof kind) hook
-
(* Admitted *)
let warn_let_as_axiom =
@@ -319,7 +312,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 =
@@ -337,9 +330,7 @@ let universe_proof_terminator compute_guard hook =
(hook (Some (fst proof.Proof_global.universes))) is_opaque in
begin match idopt with
| None -> save_named ~export_seff proof
- | Some ((_,id),None) -> save_anonymous ~export_seff proof id
- | Some ((_,id),Some kind) ->
- save_anonymous_with_strength ~export_seff proof kind id
+ | Some (_,id) -> save_anonymous ~export_seff proof id
end;
check_exist exports
end
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index bb5be4cb0..fb7c72941 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)
(***********************)
@@ -1416,7 +1416,7 @@ let add_notation_extra_printing_rule df k v =
(* Infix notations *)
-let inject_var x = CRef (Ident (Loc.ghost, Id.of_string x),None)
+let inject_var x = CAst.make @@ CRef (Ident (Loc.tag @@ Id.of_string x),None)
let add_infix local ((loc,inf),modifiers) pr sc =
check_infix_modifiers modifiers;
@@ -1477,7 +1477,7 @@ let add_class_scope scope cl =
(* Check if abbreviation to a name and avoid early insertion of
maximal implicit arguments *)
let try_interp_name_alias = function
- | [], CRef (ref,_) -> intern_reference ref
+ | [], { CAst.v = CRef (ref,_) } -> intern_reference ref
| _ -> raise Not_found
let add_syntactic_definition ident (vars,c) local onlyparse =
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index c43816c9c..64c156030 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 =
@@ -556,8 +556,7 @@ let declare_mutual_definition l =
List.map3 compute_possible_guardness_evidences
wfl fixdefs fixtypes in
let indexes =
- Pretyping.search_guard
- Loc.ghost (Global.env())
+ Pretyping.search_guard (Global.env())
possible_indexes fixdecls in
Some indexes,
List.map_i (fun i _ ->
@@ -682,7 +681,7 @@ let init_prog_info ?(opaque = false) sign n pl b t ctx deps fixkind
assert(Int.equal (Array.length obls) 0);
let n = Nameops.add_suffix n "_obligation" in
[| { obl_name = n; obl_body = None;
- obl_location = Loc.ghost, Evar_kinds.InternalHole; obl_type = t;
+ obl_location = Loc.tag Evar_kinds.InternalHole; obl_type = t;
obl_status = false, Evar_kinds.Expand; obl_deps = Int.Set.empty;
obl_tac = None } |],
mkVar n
@@ -1000,7 +999,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 fabd11260..10207d0e0 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -90,7 +90,8 @@ 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 -> CHole (fst n, None, Misctypes.IntroAnonymous, None))
+ | Vernacexpr.DefExpr(n,c,t) -> (n,Some c, match t with Some c -> c
+ | None -> CAst.make ?loc:(fst n) @@ CHole (None, Misctypes.IntroAnonymous, None))
let binders_of_decls = List.map binder_of_decl
@@ -102,14 +103,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
+ | CLocalPattern (loc,(_,_)) ->
+ 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
@@ -118,7 +119,7 @@ let typecheck_params_and_fields def id pl t ps nots fs =
let env = push_rel_context newps env0 in
let poly =
match t with
- | CSort (_, Misctypes.GType []) -> true | _ -> false in
+ | { CAst.v = CSort (Misctypes.GType []) } -> true | _ -> false in
let s = interp_type_evars env evars ~impls:empty_internalization_env t in
let sred = Reductionops.whd_all env !evars s in
let s = EConstr.Unsafe.to_constr s in
@@ -131,7 +132,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 6d9d71a62..bbf2ed4fc 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -260,8 +260,6 @@ let emacs_logger = gen_logger Emacs.quote_info Emacs.quote_warning
(* This is specific to the toplevel *)
let pr_loc loc =
- if Loc.is_ghost loc then str"<unknown>"
- else
let fname = loc.Loc.fname in
if CString.equal fname "" then
Loc.(str"Toplevel input, characters " ++ int loc.bp ++
@@ -275,7 +273,7 @@ let pr_loc loc =
let print_err_exn ?extra any =
let (e, info) = CErrors.push any in
let loc = Loc.get_loc info in
- let msg_loc = pr_loc (Option.default Loc.ghost loc) in
+ let msg_loc = Option.cata pr_loc (mt ()) loc in
let pre_hdr = pr_opt_no_spc (fun x -> x) extra ++ msg_loc in
let msg = CErrors.iprint (e, info) ++ fnl () in
std_logger ~pre_hdr Feedback.Error msg
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 6c5b0dfb4..f75e04383 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,9 +641,9 @@ 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.ghost,id)]) export
+ Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)]) export
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)
@@ -662,13 +662,13 @@ 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
(fun (export,id) ->
Option.iter
- (fun export -> vernac_import export [Ident (Loc.ghost,id)]) export
+ (fun export -> vernac_import export [Ident (Loc.tag id)]) export
) argsexport
| _::_ ->
let binders_ast = List.map
@@ -680,15 +680,15 @@ 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.ghost,id)])
+ Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)])
export
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,13 +709,13 @@ 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
(fun (export,id) ->
Option.iter
- (fun export -> vernac_import export [Ident (Loc.ghost,id)]) export
+ (fun export -> vernac_import export [Ident (Loc.tag id)]) export
) argsexport
| _ :: _ ->
@@ -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 *)
@@ -1176,10 +1176,10 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
end;
if scopes_specified || clear_scopes_flag then begin
- let scopes = List.map (Option.map (fun (o,k) ->
+ let scopes = List.map (Option.map (fun (loc,k) ->
try ignore (Notation.find_scope k); k
with UserError _ ->
- Notation.find_delimiters_scope o k)) scopes
+ Notation.find_delimiters_scope ?loc k)) scopes
in
vernac_arguments_scope locality reference scopes
end;
@@ -1515,14 +1515,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
@@ -1584,10 +1584,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 *)
@@ -1595,7 +1595,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
@@ -1609,7 +1609,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)
@@ -1654,7 +1654,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) ->
@@ -1671,7 +1671,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
@@ -1690,7 +1690,7 @@ let interp_search_about_item env =
| SearchString (s,sc) ->
try
let ref =
- Notation.interp_notation_as_global_reference Loc.ghost
+ Notation.interp_notation_as_global_reference
(fun _ -> true) s sc in
GlobSearchSubPattern (Pattern.PRef ref)
with UserError _ ->
@@ -1718,8 +1718,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 ->
@@ -1753,8 +1753,8 @@ let vernac_search ~loc s gopt r =
let vernac_locate = let open Feedback in function
| LocateAny (AN qid) -> msg_notice (print_located_qualid qid)
| LocateTerm (AN qid) -> msg_notice (print_located_term qid)
- | LocateAny (ByNotation (_, ntn, sc)) (** TODO : handle Ltac notations *)
- | LocateTerm (ByNotation (_, ntn, sc)) ->
+ | LocateAny (ByNotation (_, (ntn, sc))) (** TODO : handle Ltac notations *)
+ | LocateTerm (ByNotation (_, (ntn, sc))) ->
msg_notice
(Notation.locate_notation
(Constrextern.without_symbols pr_lglob_constr) ntn sc)
@@ -1894,7 +1894,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
@@ -2026,11 +2026,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")
@@ -2046,15 +2046,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
@@ -2129,10 +2129,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
@@ -2199,8 +2199,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 ())
@@ -2212,7 +2212,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 ());
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index fb2899515..f75f7656d 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -18,7 +18,7 @@ val vernac_require :
val interp :
?verbosely:bool ->
?proof:Proof_global.closed_proof ->
- Loc.t * Vernacexpr.vernac_expr -> unit
+ Vernacexpr.vernac_expr Loc.located -> unit
(** Prepare a "match" template for a given inductive type.
For each branch of the match, we list the constructor name
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 21:06:01 +0000