aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/auto_ind_decl.ml27
-rw-r--r--vernac/classes.ml21
-rw-r--r--vernac/command.ml138
-rw-r--r--vernac/explainErr.ml7
-rw-r--r--vernac/explainErr.mli2
-rw-r--r--vernac/himsg.ml6
-rw-r--r--vernac/ind_tables.ml2
-rw-r--r--vernac/indschemes.ml66
-rw-r--r--vernac/indschemes.mli2
-rw-r--r--vernac/lemmas.ml30
-rw-r--r--vernac/locality.ml10
-rw-r--r--vernac/metasyntax.ml74
-rw-r--r--vernac/obligations.ml19
-rw-r--r--vernac/record.ml24
-rw-r--r--vernac/search.ml1
-rw-r--r--vernac/topfmt.ml4
-rw-r--r--vernac/vernacentries.ml299
-rw-r--r--vernac/vernacentries.mli2
18 files changed, 342 insertions, 392 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index f363deac69..b99ccbf4a2 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -57,16 +57,15 @@ 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 *)
let bb = constr_of_global Coqlib.glob_bool
-let andb_prop = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb_prop
+let andb_prop = fun _ -> Universes.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb_prop
let andb_true_intro = fun _ ->
+ Universes.constr_of_global
(Coqlib.build_bool_type()).Coqlib.andb_true_intro
let tt = constr_of_global Coqlib.glob_true
@@ -75,9 +74,9 @@ let ff = constr_of_global Coqlib.glob_false
let eq = constr_of_global Coqlib.glob_eq
-let sumbool = Coqlib.build_coq_sumbool
+let sumbool () = Universes.constr_of_global (Coqlib.build_coq_sumbool ())
-let andb = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb
+let andb = fun _ -> Universes.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb
let induct_on c = induction false None c None None
@@ -85,12 +84,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 =
@@ -534,7 +533,7 @@ open Namegen
let compute_bl_goal ind lnamesparrec nparrec =
let eqI, eff = eqI ind lnamesparrec in
let list_id = list_id lnamesparrec in
- let avoid = List.fold_right (Nameops.name_fold (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
+ let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
let create_input c =
let x = next_ident_away (Id.of_string "x") avoid and
y = next_ident_away (Id.of_string "y") avoid in
@@ -608,8 +607,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 }
]);
(*
@@ -677,7 +676,7 @@ let _ = bl_scheme_kind_aux := fun () -> bl_scheme_kind
let compute_lb_goal ind lnamesparrec nparrec =
let list_id = list_id lnamesparrec in
let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in
- let avoid = List.fold_right (Nameops.name_fold (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
+ let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
let eqI, eff = eqI ind lnamesparrec in
let create_input c =
let x = next_ident_away (Id.of_string "x") avoid and
@@ -807,7 +806,7 @@ let compute_dec_goal ind lnamesparrec nparrec =
check_not_is_defined ();
let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in
let list_id = list_id lnamesparrec in
- let avoid = List.fold_right (Nameops.name_fold (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
+ let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
let create_input c =
let x = next_ident_away (Id.of_string "x") avoid and
y = next_ident_away (Id.of_string "y") avoid in
@@ -851,7 +850,7 @@ let compute_dec_goal ind lnamesparrec nparrec =
create_input (
mkNamedProd n (mkFullInd ind (2*nparrec)) (
mkNamedProd m (mkFullInd ind (2*nparrec+1)) (
- mkApp(sumbool(),[|eqnm;mkApp (Coqlib.build_coq_not(),[|eqnm|])|])
+ mkApp(sumbool(),[|eqnm;mkApp (Universes.constr_of_global @@ Coqlib.build_coq_not(),[|eqnm|])|])
)
)
)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index d515b0c9b2..004083dcf9 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -32,7 +32,6 @@ open Entries
let refine_instance = ref true
let _ = Goptions.declare_bool_option {
- Goptions.optsync = true;
Goptions.optdepr = false;
Goptions.optname = "definition of instances by refining";
Goptions.optkey = ["Refine";"Instance";"Mode"];
@@ -75,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.")
@@ -145,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 =
@@ -215,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)
@@ -235,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
@@ -255,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
@@ -354,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 =
@@ -380,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) =
@@ -406,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 2fa2aa4e33..87e7e50ec2 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 *)
@@ -210,7 +211,7 @@ let do_definition ident k pl bl red_option c ctypopt hook =
assert(Univ.ContextSet.is_empty ctx);
let typ = match ce.const_entry_type with
| Some t -> t
- | None -> EConstr.Unsafe.to_constr (Retyping.get_type_of env evd (EConstr.of_constr c))
+ | None -> EConstr.to_constr evd (Retyping.get_type_of env evd (EConstr.of_constr c))
in
Obligations.check_evars env evd;
let obls, _, c, cty =
@@ -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
@@ -381,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 ++
@@ -410,8 +411,8 @@ let mk_mltype_data evdref env assums arity indname =
(is_ml_type,indname,assums)
let prepare_param = function
- | LocalAssum (na,t) -> out_name na, LocalAssumEntry t
- | LocalDef (na,b,_) -> out_name na, LocalDefEntry b
+ | LocalAssum (na,t) -> Name.get_id na, LocalAssumEntry t
+ | LocalDef (na,b,_) -> Name.get_id na, LocalDefEntry b
(** Make the arity conclusion flexible to avoid generating an upper bound universe now,
only if the universe does not appear anywhere else.
@@ -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
@@ -589,7 +590,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
(* Names of parameters as arguments of the inductive type (defs removed) *)
let assums = List.filter is_local_assum ctx_params in
- let params = List.map (RelDecl.get_name %> out_name) assums in
+ let params = List.map (RelDecl.get_name %> Name.get_id) assums in
(* Interpret the arities *)
let arities = List.map (interp_ind_arity env_params evdref) indl in
@@ -675,14 +676,14 @@ 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 =
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
@@ -714,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
@@ -905,23 +906,27 @@ let subtac_dir = [contrib_name]
let fixsub_module = subtac_dir @ ["Wf"]
let tactics_module = subtac_dir @ ["Tactics"]
-let init_reference dir s () = Coqlib.gen_reference "Command" dir s
-let init_constant dir s () = EConstr.of_constr (Coqlib.gen_constant "Command" dir s)
+let init_reference dir s () = Coqlib.coq_reference "Command" dir s
+let init_constant dir s evdref =
+ let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map !evdref)
+ (Coqlib.coq_reference "Command" dir s)
+ in evdref := Sigma.to_evar_map sigma; c
+
let make_ref l s = init_reference l s
let fix_proto = init_constant tactics_module "fix_proto"
let fix_sub_ref = make_ref fixsub_module "Fix_sub"
let measure_on_R_ref = make_ref fixsub_module "MR"
let well_founded = init_constant ["Init"; "Wf"] "well_founded"
-let mkSubset name typ prop =
+let mkSubset evdref name typ prop =
let open EConstr in
- mkApp (EConstr.of_constr (Universes.constr_of_global (delayed_force build_sigma).typ),
+ mkApp (Evarutil.e_new_global evdref (delayed_force build_sigma).typ,
[| 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 =
+let rec telescope evdref l =
let open EConstr in
let open Vars in
match l with
@@ -933,10 +938,8 @@ let rec telescope l =
(fun (ty, tys, (k, constr)) decl ->
let t = RelDecl.get_type decl in
let pred = mkLambda (RelDecl.get_name decl, t, ty) in
- let ty = Universes.constr_of_global (Lazy.force sigT).typ in
- let ty = EConstr.of_constr ty in
- let intro = Universes.constr_of_global (Lazy.force sigT).intro in
- let intro = EConstr.of_constr intro in
+ let ty = Evarutil.e_new_global evdref (Lazy.force sigT).typ in
+ let intro = Evarutil.e_new_global evdref (Lazy.force sigT).intro in
let sigty = mkApp (ty, [|t; pred|]) in
let intro = mkApp (intro, [|lift k t; lift k pred; mkRel k; constr|]) in
(sigty, pred :: tys, (succ k, intro)))
@@ -945,17 +948,15 @@ let rec telescope l =
let (last, subst) = List.fold_right2
(fun pred decl (prev, subst) ->
let t = RelDecl.get_type decl in
- let p1 = Universes.constr_of_global (Lazy.force sigT).proj1 in
- let p1 = EConstr.of_constr p1 in
- let p2 = Universes.constr_of_global (Lazy.force sigT).proj2 in
- let p2 = EConstr.of_constr p2 in
+ let p1 = Evarutil.e_new_global evdref (Lazy.force sigT).proj1 in
+ let p2 = Evarutil.e_new_global evdref (Lazy.force sigT).proj2 in
let proj1 = applist (p1, [t; pred; prev]) in
let proj2 = applist (p2, [t; pred; prev]) in
(lift 1 proj2, LocalDef (get_name decl, proj1, t) :: subst))
(List.rev tys) tl (mkRel 1, [])
in ty, (LocalDef (n, last, t) :: subst), constr
- | LocalDef (n, b, t) :: tl -> let ty, subst, term = telescope tl in
+ | LocalDef (n, b, t) :: tl -> let ty, subst, term = telescope evdref tl in
ty, (LocalDef (n, b, t) :: subst), lift 1 term
let nf_evar_context sigma ctx =
@@ -974,7 +975,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let top_env = push_rel_context binders_rel env in
let top_arity = interp_type_evars top_env evdref arityc in
let full_arity = it_mkProd_or_LetIn top_arity binders_rel in
- let argtyp, letbinders, make = telescope binders_rel in
+ let argtyp, letbinders, make = telescope evdref binders_rel in
let argname = Id.of_string "recarg" in
let arg = LocalAssum (Name argname, argtyp) in
let binders = letbinders @ [arg] in
@@ -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
@@ -1002,7 +1003,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
it_mkLambda_or_LetIn measure letbinders,
it_mkLambda_or_LetIn measure binders
in
- let comb = EConstr.of_constr (Universes.constr_of_global (delayed_force measure_on_R_ref)) in
+ let comb = Evarutil.e_new_global evdref (delayed_force measure_on_R_ref) in
let relargty = EConstr.of_constr relargty in
let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in
let wf_rel_fun x y =
@@ -1010,15 +1011,15 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
subst1 y measure_body |])
in wf_rel, wf_rel_fun, measure
in
- let wf_proof = mkApp (delayed_force well_founded, [| argtyp ; wf_rel |]) in
+ let wf_proof = mkApp (well_founded evdref, [| argtyp ; wf_rel |]) in
let argid' = Id.of_string (Id.to_string argname ^ "'") in
let wfarg len = LocalAssum (Name argid',
- mkSubset (Name argid') argtyp
+ mkSubset evdref (Name argid') argtyp
(wf_rel_fun (mkRel 1) (mkRel (len + 1))))
in
let intern_bl = wfarg 1 :: [arg] in
let _intern_env = push_rel_context intern_bl env in
- let proj = (*FIXME*)EConstr.of_constr (Universes.constr_of_global (delayed_force build_sigma).Coqlib.proj1) in
+ let proj = Evarutil.e_new_global evdref (delayed_force build_sigma).Coqlib.proj1 in
let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in
let projection = (* in wfarg :: arg :: before *)
mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |])
@@ -1031,7 +1032,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let intern_fun_binder = LocalAssum (Name (add_suffix recname "'"), intern_fun_arity_prod) in
let curry_fun =
let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in
- let intro = (*FIXME*)EConstr.of_constr (Universes.constr_of_global (delayed_force build_sigma).Coqlib.intro) in
+ let intro = Evarutil.e_new_global evdref (delayed_force build_sigma).Coqlib.intro in
let arg = mkApp (intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in
let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in
let rcurry = mkApp (rel, [| measure; lift len measure |]) in
@@ -1057,10 +1058,10 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
let prop = mkLambda (Name argname, argtyp, top_arity_let) in
let def =
- mkApp (EConstr.of_constr (Universes.constr_of_global (delayed_force fix_sub_ref)),
+ mkApp (Evarutil.e_new_global evdref (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,Anonymous)) wf_proof;
prop |])
in
let def = Typing.e_solve_evars env evdref def in
@@ -1073,12 +1074,12 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
if List.length binders_rel > 1 then
let name = add_suffix recname "_func" in
let hook l gr _ =
- let body = it_mkLambda_or_LetIn (mkApp (EConstr.of_constr (Universes.constr_of_global gr), [|make|])) binders_rel in
+ let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in
let ty = it_mkProd_or_LetIn top_arity binders_rel in
let ty = EConstr.Unsafe.to_constr ty in
let pl, univs = Evd.universe_context ?names:pl !evdref in
(*FIXME poly? *)
- let ce = definition_entry ~poly ~types:ty ~univs (EConstr.Unsafe.to_constr (Evarutil.nf_evar !evdref body)) in
+ let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in
(** FIXME: include locality *)
let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
let gr = ConstRef c in
@@ -1095,10 +1096,8 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
in hook, recname, typ
in
let hook = Lemmas.mk_hook hook in
- let fullcoqc = Evarutil.nf_evar !evdref def in
- let fullctyp = Evarutil.nf_evar !evdref typ in
- let fullcoqc = EConstr.Unsafe.to_constr fullcoqc in
- let fullctyp = EConstr.Unsafe.to_constr fullctyp in
+ let fullcoqc = EConstr.to_constr !evdref def in
+ let fullctyp = EConstr.to_constr !evdref typ in
Obligations.check_evars env !evdref;
let evars, _, evars_def, evars_typ =
Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp
@@ -1121,7 +1120,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
@@ -1141,7 +1140,7 @@ let interp_recursive isfix fixl notations =
let sort = Evarutil.evd_comb1 (Typing.type_of ~refresh:true env) evdref t in
let fixprot =
try
- let app = mkApp (delayed_force fix_proto, [|sort; t|]) in
+ let app = mkApp (fix_proto evdref, [|sort; t|]) in
Typing.e_solve_evars env evdref app
with e when CErrors.noncritical e -> t
in
@@ -1210,7 +1209,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 =
@@ -1261,8 +1260,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
@@ -1281,7 +1280,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
@@ -1301,9 +1300,9 @@ let do_program_recursive local p fixkind fixl ntns =
let collect_evars id def typ imps =
(* Generalize by the recursive prototypes *)
let def =
- EConstr.Unsafe.to_constr (nf_evar evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign))
+ EConstr.to_constr evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign)
and typ =
- EConstr.Unsafe.to_constr (nf_evar evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign))
+ EConstr.to_constr evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign)
in
let evm = collect_evars_of_term evd def typ in
let evars, _, def, typ =
@@ -1322,8 +1321,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 +1348,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 04841c922e..040c86805e 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 370ad7e3b5..9202729cee 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/himsg.ml b/vernac/himsg.ml
index 17bb87f2aa..6d8dd82ac6 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -682,12 +682,12 @@ let explain_wrong_abstraction_type env sigma na abs expected result =
let explain_abstraction_over_meta _ m n =
strbrk "Too complex unification problem: cannot find a solution for both " ++
- pr_name m ++ spc () ++ str "and " ++ pr_name n ++ str "."
+ Name.print m ++ spc () ++ str "and " ++ Name.print n ++ str "."
let explain_non_linear_unification env sigma m t =
let t = EConstr.to_constr sigma t in
strbrk "Cannot unambiguously instantiate " ++
- pr_name m ++ str ":" ++
+ Name.print m ++ str ":" ++
strbrk " which would require to abstract twice on " ++
pr_lconstr_env env sigma t ++ str "."
@@ -1055,7 +1055,7 @@ let explain_refiner_bad_type arg ty conclty =
let explain_refiner_unresolved_bindings l =
str "Unable to find an instance for the " ++
str (String.plural (List.length l) "variable") ++ spc () ++
- prlist_with_sep pr_comma pr_name l ++ str"."
+ prlist_with_sep pr_comma Name.print l ++ str"."
let explain_refiner_cannot_apply t harg =
str "In refiner, a term of type" ++ brk(1,1) ++
diff --git a/vernac/ind_tables.ml b/vernac/ind_tables.ml
index c6588684a4..f3259f1f3b 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 9ba4e46e48..a678d20bba 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -45,8 +45,7 @@ open Context.Rel.Declaration
let elim_flag = ref true
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "automatic declaration of induction schemes";
optkey = ["Elimination";"Schemes"];
optread = (fun () -> !elim_flag) ;
@@ -55,16 +54,14 @@ let _ =
let bifinite_elim_flag = ref false
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "automatic declaration of induction schemes for non-recursive types";
optkey = ["Nonrecursive";"Elimination";"Schemes"];
optread = (fun () -> !bifinite_elim_flag) ;
optwrite = (fun b -> bifinite_elim_flag := b) }
let _ =
declare_bool_option
- { optsync = true;
- optdepr = true; (* compatibility 2014-09-03*)
+ { optdepr = true; (* compatibility 2014-09-03*)
optname = "automatic declaration of induction schemes for non-recursive types";
optkey = ["Record";"Elimination";"Schemes"];
optread = (fun () -> !bifinite_elim_flag) ;
@@ -73,8 +70,7 @@ let _ =
let case_flag = ref false
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "automatic declaration of case analysis schemes";
optkey = ["Case";"Analysis";"Schemes"];
optread = (fun () -> !case_flag) ;
@@ -83,16 +79,14 @@ let _ =
let eq_flag = ref false
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "automatic declaration of boolean equality";
optkey = ["Boolean";"Equality";"Schemes"];
optread = (fun () -> !eq_flag) ;
optwrite = (fun b -> eq_flag := b) }
let _ = (* compatibility *)
declare_bool_option
- { optsync = true;
- optdepr = true;
+ { optdepr = true;
optname = "automatic declaration of boolean equality";
optkey = ["Equality";"Scheme"];
optread = (fun () -> !eq_flag) ;
@@ -103,8 +97,7 @@ let is_eq_flag () = !eq_flag && Flags.version_strictly_greater Flags.V8_2
let eq_dec_flag = ref false
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "automatic declaration of decidable equality";
optkey = ["Decidable";"Equality";"Schemes"];
optread = (fun () -> !eq_dec_flag) ;
@@ -113,8 +106,7 @@ let _ =
let rewriting_flag = ref false
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname ="automatic declaration of rewriting schemes for equality types";
optkey = ["Rewriting";"Schemes"];
optread = (fun () -> !rewriting_flag) ;
@@ -379,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
@@ -426,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
@@ -437,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
@@ -461,11 +453,19 @@ let fold_left' f = function
[] -> invalid_arg "fold_left'"
| hd :: tl -> List.fold_left f hd tl
+let new_global sigma gr =
+ let open Sigma in
+ let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map sigma) gr
+ in Sigma.to_evar_map sigma, c
+
+let mk_coq_and sigma = new_global sigma (Coqlib.build_coq_and ())
+let mk_coq_conj sigma = new_global sigma (Coqlib.build_coq_conj ())
+
let build_combined_scheme env schemes =
- let defs = List.map (fun cst -> (* FIXME *)
- let evd, c = Evd.fresh_constant_instance env (Evd.from_env env) cst in
- (c, Typeops.type_of_constant_in env c)) schemes in
-(* let nschemes = List.length schemes in *)
+ let evdref = ref (Evd.from_env env) in
+ let defs = List.map (fun cst ->
+ let evd, c = Evd.fresh_constant_instance env !evdref cst in
+ evdref := evd; (c, Typeops.type_of_constant_in env c)) schemes in
let find_inductive ty =
let (ctx, arity) = decompose_prod ty in
let (_, last) = List.hd ctx in
@@ -479,25 +479,27 @@ let build_combined_scheme env schemes =
let (c, t) = List.hd defs in
let ctx, ind, nargs = find_inductive t in
(* Number of clauses, including the predicates quantification *)
- let prods = nb_prod Evd.empty (EConstr.of_constr t) - (nargs + 1) (** FIXME *) in
- let coqand = Coqlib.build_coq_and () and coqconj = Coqlib.build_coq_conj () in
+ let prods = nb_prod !evdref (EConstr.of_constr t) - (nargs + 1) in
+ let sigma, coqand = mk_coq_and !evdref in
+ let sigma, coqconj = mk_coq_conj sigma in
+ let () = evdref := sigma in
let relargs = rel_vect 0 prods in
let concls = List.rev_map
- (fun (cst, t) -> (* FIXME *)
+ (fun (cst, t) ->
mkApp(mkConstU cst, relargs),
snd (decompose_prod_n prods t)) defs in
let concl_bod, concl_typ =
fold_left'
(fun (accb, acct) (cst, x) ->
- mkApp (coqconj, [| x; acct; cst; accb |]),
- mkApp (coqand, [| x; acct |])) concls
+ mkApp (EConstr.to_constr !evdref coqconj, [| x; acct; cst; accb |]),
+ mkApp (EConstr.to_constr !evdref coqand, [| x; acct |])) concls
in
let ctx, _ =
list_split_rev_at prods
(List.rev_map (fun (x, y) -> LocalAssum (x, y)) ctx) in
let typ = List.fold_left (fun d c -> Term.mkProd_wo_LetIn c d) concl_typ ctx in
let body = it_mkLambda_or_LetIn concl_bod ctx in
- (body, typ)
+ (!evdref, body, typ)
let do_combined_scheme name schemes =
let csts =
@@ -505,12 +507,12 @@ 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
+ let sigma,body,typ = build_combined_scheme (Global.env ()) csts in
let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
- ignore (define (snd name) UserIndividualRequest Evd.empty proof_output (Some typ));
+ ignore (define (snd name) UserIndividualRequest sigma proof_output (Some typ));
fixpoint_message None [snd name]
(**********************************************************************)
diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli
index e5d79fd514..0f559d2bd8 100644
--- a/vernac/indschemes.mli
+++ b/vernac/indschemes.mli
@@ -40,7 +40,7 @@ val do_scheme : (Id.t located option * scheme) list -> unit
(** Combine a list of schemes into a conjunction of them *)
-val build_combined_scheme : env -> constant list -> constr * types
+val build_combined_scheme : env -> constant list -> Evd.evar_map * constr * types
val do_combined_scheme : Id.t located -> Id.t located list -> unit
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index b79795aebd..d6ae0ea86f 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) }
@@ -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
@@ -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
@@ -273,20 +273,13 @@ 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
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
@@ -474,8 +465,7 @@ let keep_admitted_vars = ref true
let _ =
let open Goptions in
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "keep section variables in admitted proofs";
optkey = ["Keep"; "Admitted"; "Variables"];
optread = (fun () -> !keep_admitted_vars);
@@ -488,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 03640676e6..a25acb0d34 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 bb5be4cb05..42494dd28a 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,12 +187,12 @@ 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 = Loc.add_loc info loc in
+ let info = Option.cata (Loc.add_loc info) info loc in
iraise (e, info)
(***********************)
@@ -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 *)
@@ -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 24cb9c886e..47ac16f9c7 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 =
@@ -221,7 +221,7 @@ let eterm_obligations env name evm fs ?status t ty =
in
let loc, k = evar_source id evm in
let status = match k with
- | Evar_kinds.QuestionMark o -> o
+ | Evar_kinds.QuestionMark (o,_) -> o
| _ -> match status with
| Some o -> o
| None -> Evar_kinds.Define (not (Program.get_proofs_transparency ()))
@@ -260,7 +260,7 @@ let eterm_obligations env name evm fs ?status t ty =
let tactics_module = ["Program";"Tactics"]
let safe_init_constant md name () =
Coqlib.check_required_library ("Coq"::md);
- Coqlib.gen_constant "Obligations" md name
+ Universes.constr_of_global (Coqlib.coq_reference "Obligations" md name)
let hide_obligation = safe_init_constant tactics_module "obligation"
let pperror cmd = CErrors.user_err ~hdr:"Program" cmd
@@ -340,8 +340,7 @@ let get_hide_obligations () = !hide_obligations
open Goptions
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "Hidding of Program obligations";
optkey = ["Hide";"Obligations"];
optread = get_hide_obligations;
@@ -354,8 +353,7 @@ let get_shrink_obligations () = !shrink_obligations
let _ =
declare_bool_option
- { optsync = true;
- optdepr = true;
+ { optdepr = true;
optname = "Shrinking of Program obligations";
optkey = ["Shrink";"Obligations"];
optread = get_shrink_obligations;
@@ -558,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 _ ->
@@ -684,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
@@ -1002,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 53722b8f61..5accc8e379 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -35,8 +35,7 @@ module RelDecl = Context.Rel.Declaration
let primitive_flag = ref false
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "use of primitive projections";
optkey = ["Primitive";"Projections"];
optread = (fun () -> !primitive_flag) ;
@@ -45,8 +44,7 @@ let _ =
let typeclasses_strict = ref false
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "strict typeclass resolution";
optkey = ["Typeclasses";"Strict";"Resolution"];
optread = (fun () -> !typeclasses_strict);
@@ -55,8 +53,7 @@ let _ =
let typeclasses_unique = ref false
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "unique typeclass instances";
optkey = ["Typeclasses";"Unique";"Instances"];
optread = (fun () -> !typeclasses_unique);
@@ -93,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
@@ -105,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
@@ -121,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
@@ -134,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
@@ -563,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/search.ml b/vernac/search.ml
index 5b6e9a9c3c..9160158003 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -40,7 +40,6 @@ module SearchBlacklist =
let title = "Current search blacklist : "
let member_message s b =
str "Search blacklist does " ++ (if b then mt () else str "not ") ++ str "include " ++ str s
- let synchronous = true
end)
(* The functions iter_constructors and iter_declarations implement the behavior
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index 6d9d71a62b..bbf2ed4fcf 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 d4e6af9959..77be7f454a 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))
@@ -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 *)
@@ -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
@@ -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
@@ -631,25 +631,25 @@ 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
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)
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 ();
@@ -662,39 +662,39 @@ 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
(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
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
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
| [] ->
@@ -709,32 +709,32 @@ 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
| _ :: _ ->
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
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 *)
@@ -843,11 +843,10 @@ let focus_command_cond = Proof.no_cond command_focus
let vernac_solve_existential = instantiate_nth_evar_com
let vernac_set_end_tac tac =
- let open Genintern in
- let env = { genv = Global.env (); ltacvars = Id.Set.empty } in
+ 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*)
@@ -904,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()))
@@ -973,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";
@@ -1004,12 +1003,12 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
let err_extra_args names =
user_err ~hdr:"vernac_declare_arguments"
(strbrk "Extra arguments: " ++
- prlist_with_sep pr_comma pr_name names ++ str ".")
+ prlist_with_sep pr_comma Name.print names ++ str ".")
in
let err_missing_args names =
user_err ~hdr:"vernac_declare_arguments"
(strbrk "The following arguments are not declared: " ++
- prlist_with_sep pr_comma pr_name names ++ str ".")
+ prlist_with_sep pr_comma Name.print names ++ str ".")
in
let rec check_extra_args extra_args =
@@ -1019,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 =
@@ -1033,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
@@ -1063,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
@@ -1094,14 +1093,14 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
match !example_renaming with
| None -> mt ()
| Some (o,n) ->
- str "Argument " ++ pr_name o ++
- str " renamed to " ++ pr_name n ++ str ".");
+ str "Argument " ++ Name.print o ++
+ str " renamed to " ++ Name.print n ++ str ".");
let duplicate_names =
List.duplicates Name.equal (List.filter ((!=) Anonymous) names)
in
if not (List.is_empty duplicate_names) then begin
- let duplicates = prlist_with_sep pr_comma pr_name duplicate_names in
+ let duplicates = prlist_with_sep pr_comma Name.print duplicate_names in
user_err (strbrk "Some argument names are duplicated: " ++ duplicates)
end;
@@ -1130,7 +1129,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
anonymous argument implicit *)
| Anonymous :: _, (name, _) :: _ ->
user_err ~hdr:"vernac_declare_arguments"
- (strbrk"Argument "++ pr_name name ++
+ (strbrk"Argument "++ Name.print name ++
strbrk " cannot be declared implicit.")
| Name id :: inf_names, (name, impl) :: implicits ->
@@ -1144,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)
@@ -1176,10 +1175,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;
@@ -1228,8 +1227,7 @@ let vernac_generalizable locality =
let _ =
declare_bool_option
- { optsync = false;
- optdepr = false;
+ { optdepr = false;
optname = "silent";
optkey = ["Silent"];
optread = (fun () -> !Flags.quiet);
@@ -1237,8 +1235,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "implicit arguments";
optkey = ["Implicit";"Arguments"];
optread = Impargs.is_implicit_args;
@@ -1246,8 +1243,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "strict implicit arguments";
optkey = ["Strict";"Implicit"];
optread = Impargs.is_strict_implicit_args;
@@ -1255,8 +1251,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "strong strict implicit arguments";
optkey = ["Strongly";"Strict";"Implicit"];
optread = Impargs.is_strongly_strict_implicit_args;
@@ -1264,8 +1259,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "contextual implicit arguments";
optkey = ["Contextual";"Implicit"];
optread = Impargs.is_contextual_implicit_args;
@@ -1273,8 +1267,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "implicit status of reversible patterns";
optkey = ["Reversible";"Pattern";"Implicit"];
optread = Impargs.is_reversible_pattern_implicit_args;
@@ -1282,8 +1275,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "maximal insertion of implicit";
optkey = ["Maximal";"Implicit";"Insertion"];
optread = Impargs.is_maximal_implicit_args;
@@ -1291,8 +1283,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "automatic introduction of variables";
optkey = ["Automatic";"Introduction"];
optread = Flags.is_auto_intros;
@@ -1300,8 +1291,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "coercion printing";
optkey = ["Printing";"Coercions"];
optread = (fun () -> !Constrextern.print_coercions);
@@ -1309,8 +1299,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "printing of existential variable instances";
optkey = ["Printing";"Existential";"Instances"];
optread = (fun () -> !Detyping.print_evar_arguments);
@@ -1318,8 +1307,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "implicit arguments printing";
optkey = ["Printing";"Implicit"];
optread = (fun () -> !Constrextern.print_implicits);
@@ -1327,8 +1315,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "implicit arguments defensive printing";
optkey = ["Printing";"Implicit";"Defensive"];
optread = (fun () -> !Constrextern.print_implicits_defensive);
@@ -1336,8 +1323,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "projection printing using dot notation";
optkey = ["Printing";"Projections"];
optread = (fun () -> !Constrextern.print_projections);
@@ -1345,8 +1331,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "notations printing";
optkey = ["Printing";"Notations"];
optread = (fun () -> not !Constrextern.print_no_symbol);
@@ -1354,8 +1339,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "raw printing";
optkey = ["Printing";"All"];
optread = (fun () -> !Flags.raw_print);
@@ -1363,8 +1347,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "use of the program extension";
optkey = ["Program";"Mode"];
optread = (fun () -> !Flags.program_mode);
@@ -1372,8 +1355,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "universe polymorphism";
optkey = ["Universe"; "Polymorphism"];
optread = Flags.is_universe_polymorphism;
@@ -1381,8 +1363,7 @@ let _ =
let _ =
declare_int_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "the level of inlining during functor application";
optkey = ["Inline";"Level"];
optread = (fun () -> Some (Flags.get_inline_level ()));
@@ -1392,8 +1373,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "kernel term sharing";
optkey = ["Kernel"; "Term"; "Sharing"];
optread = (fun () -> !CClosure.share);
@@ -1404,8 +1384,7 @@ let _ =
let _ =
declare_int_option
- { optsync = false;
- optdepr = true;
+ { optdepr = true;
optname = "the undo limit (OBSOLETE)";
optkey = ["Undo"];
optread = (fun _ -> None);
@@ -1413,8 +1392,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "display compact goal contexts";
optkey = ["Printing";"Compact";"Contexts"];
optread = (fun () -> Printer.get_compact_context());
@@ -1422,8 +1400,7 @@ let _ =
let _ =
declare_int_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "the printing depth";
optkey = ["Printing";"Depth"];
optread = Topfmt.get_depth_boxes;
@@ -1431,8 +1408,7 @@ let _ =
let _ =
declare_int_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "the printing width";
optkey = ["Printing";"Width"];
optread = Topfmt.get_margin;
@@ -1440,8 +1416,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "printing of universes";
optkey = ["Printing";"Universes"];
optread = (fun () -> !Constrextern.print_universes);
@@ -1449,8 +1424,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "dumping bytecode after compilation";
optkey = ["Dump";"Bytecode"];
optread = Flags.get_dump_bytecode;
@@ -1458,8 +1432,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "explicitly parsing implicit arguments";
optkey = ["Parsing";"Explicit"];
optread = (fun () -> !Constrintern.parsing_explicit);
@@ -1467,8 +1440,7 @@ let _ =
let _ =
declare_string_option ~preprocess:CWarnings.normalize_flags_string
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "warnings display";
optkey = ["Warnings"];
optread = CWarnings.get_flags;
@@ -1480,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
@@ -1491,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]
@@ -1542,14 +1514,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
@@ -1611,10 +1583,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 *)
@@ -1622,7 +1594,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
@@ -1636,7 +1608,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)
@@ -1681,7 +1653,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) ->
@@ -1698,7 +1670,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
@@ -1717,7 +1689,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 _ ->
@@ -1739,15 +1711,14 @@ let search_output_name_only = ref false
let _ =
declare_bool_option
- { optsync = true;
- optdepr = false;
+ { optdepr = false;
optname = "output-name-only search";
optkey = ["Search";"Output";"Name";"Only"];
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 ->
@@ -1781,8 +1752,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)
@@ -1793,13 +1764,12 @@ 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.";
- let t = (Constrintern.global_reference (snd id)) in
- if not (isConst t) then
- error "Register inline: a constant is expected";
- let kn = destConst t in
+ user_err Pp.(str "Cannot register a primitive while in proof editing mode.");
+ let kn = Constrintern.global_reference (snd id) in
+ if not (isConstRef kn) then
+ user_err Pp.(str "Register inline: a constant is expected");
match r with
- | RegisterInline -> Global.register_inline (Univ.out_punivs kn)
+ | RegisterInline -> Global.register_inline (destConstRef kn)
(********************)
(* Proof management *)
@@ -1809,7 +1779,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)
@@ -1824,7 +1794,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.
@@ -1922,7 +1892,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
@@ -2054,11 +2024,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")
@@ -2074,15 +2044,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
@@ -2110,7 +2080,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 =
@@ -2124,7 +2094,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 ()
@@ -2137,8 +2107,7 @@ let default_timeout = ref None
let _ =
Goptions.declare_int_option
- { Goptions.optsync = true;
- Goptions.optdepr = false;
+ { Goptions.optdepr = false;
Goptions.optname = "the default timeout";
Goptions.optkey = ["Default";"Timeout"];
Goptions.optread = (fun () -> !default_timeout);
@@ -2158,10 +2127,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
@@ -2202,13 +2171,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) ->
@@ -2228,8 +2197,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 ())
@@ -2241,7 +2210,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 fb2899515f..f75f7656db 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.25.1) at 2026-05-05 05:01:00 +0000