aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/assumptions.ml4
-rw-r--r--toplevel/auto_ind_decl.ml41
-rw-r--r--toplevel/class.ml8
-rw-r--r--toplevel/classes.ml18
-rw-r--r--toplevel/command.ml36
-rw-r--r--toplevel/coqinit.ml7
-rw-r--r--toplevel/himsg.ml13
-rw-r--r--toplevel/ind_tables.ml2
-rw-r--r--toplevel/indschemes.ml2
-rw-r--r--toplevel/locality.ml2
-rw-r--r--toplevel/metasyntax.ml47
-rw-r--r--toplevel/metasyntax.mli5
-rw-r--r--toplevel/mltop.ml10
-rw-r--r--toplevel/obligations.ml24
-rw-r--r--toplevel/obligations.mli4
-rw-r--r--toplevel/record.ml34
-rw-r--r--toplevel/search.ml12
-rw-r--r--toplevel/vernac.ml2
-rw-r--r--toplevel/vernacentries.ml77
-rw-r--r--toplevel/vernacentries.mli2
-rw-r--r--toplevel/vernacinterp.ml4
21 files changed, 189 insertions, 165 deletions
diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml
index 45c539e229..8865cd6469 100644
--- a/toplevel/assumptions.ml
+++ b/toplevel/assumptions.ml
@@ -25,6 +25,8 @@ open Globnames
open Printer
open Context.Named.Declaration
+module NamedDecl = Context.Named.Declaration
+
(** For a constant c in a module sealed by an interface (M:T and
not M<:T), [Global.lookup_constant] may return a [constant_body]
without body. We fix this by looking in the implementation
@@ -144,7 +146,7 @@ let label_of = function
let rec traverse current ctx accu t = match kind_of_term t with
| Var id ->
- let body () = Global.lookup_named id |> get_value in
+ let body () = id |> Global.lookup_named |> NamedDecl.get_value in
traverse_object accu body (VarRef id)
| Const (kn, _) ->
let body () = Global.body_of_constant_body (lookup_constant kn) in
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 0561fc4b82..b1811d6a65 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -25,7 +25,8 @@ open Tactics
open Ind_tables
open Misctypes
open Proofview.Notations
-open Context.Rel.Declaration
+
+module RelDecl = Context.Rel.Declaration
let out_punivs = Univ.out_punivs
@@ -150,14 +151,14 @@ let build_beq_scheme mode kn =
( fun a b decl -> (* mkLambda(n,b,a) ) *)
(* here I leave the Naming thingy so that the type of
the function is more readable for the user *)
- mkNamedLambda (eqName (get_name decl)) b a )
+ mkNamedLambda (eqName (RelDecl.get_name decl)) b a )
c (List.rev eqs_typ) lnamesparrec
in
List.fold_left (fun a decl ->(* mkLambda(n,t,a)) eq_input rel_list *)
(* Same here , hoping the auto renaming will do something good ;) *)
mkNamedLambda
- (match get_name decl with Name s -> s | Anonymous -> Id.of_string "A")
- (get_type decl) a) eq_input lnamesparrec
+ (match RelDecl.get_name decl with Name s -> s | Anonymous -> Id.of_string "A")
+ (RelDecl.get_type decl) a) eq_input lnamesparrec
in
let make_one_eq cur =
let u = Univ.Instance.empty in
@@ -255,7 +256,7 @@ let build_beq_scheme mode kn =
| 0 -> Lazy.force tt
| _ -> let eqs = Array.make nb_cstr_args (Lazy.force tt) in
for ndx = 0 to nb_cstr_args-1 do
- let cc = get_type (List.nth constrsi.(i).cs_args ndx) in
+ let cc = RelDecl.get_type (List.nth constrsi.(i).cs_args ndx) in
let eqA, eff' = compute_A_equality rel_list
nparrec
(nparrec+3+2*nb_cstr_args)
@@ -274,14 +275,14 @@ let build_beq_scheme mode kn =
(Array.sub eqs 1 (nb_cstr_args - 1))
)
in
- (List.fold_left (fun a decl -> mkLambda (get_name decl, get_type decl, a)) cc
+ (List.fold_left (fun a decl -> mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a)) cc
(constrsj.(j).cs_args)
)
else ar2.(j) <- (List.fold_left (fun a decl ->
- mkLambda (get_name decl, get_type decl, a)) (Lazy.force ff) (constrsj.(j).cs_args) )
+ mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a)) (Lazy.force ff) (constrsj.(j).cs_args) )
done;
- ar.(i) <- (List.fold_left (fun a decl -> mkLambda (get_name decl, get_type decl, a))
+ ar.(i) <- (List.fold_left (fun a decl -> mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a))
(mkCase (ci,do_predicate rel_list nb_cstr_args,
mkVar (Id.of_string "Y") ,ar2))
(constrsi.(i).cs_args))
@@ -346,7 +347,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
let rec find i =
if Id.equal avoid.(n-i) s then avoid.(n-i-x)
else (if i<n then find (i+1)
- else errorlabstrm "AutoIndDecl.do_replace_lb"
+ else user_err ~hdr:"AutoIndDecl.do_replace_lb"
(str "Var " ++ pr_id s ++ str " seems unknown.")
)
in mkVar (find 1)
@@ -404,7 +405,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
let rec find i =
if Id.equal avoid.(n-i) s then avoid.(n-i-x)
else (if i<n then find (i+1)
- else errorlabstrm "AutoIndDecl.do_replace_bl"
+ else user_err ~hdr:"AutoIndDecl.do_replace_bl"
(str "Var " ++ pr_id s ++ str " seems unknown.")
)
in mkVar (find 1)
@@ -495,7 +496,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
[(in,eq_in,in_bl,in_al),,...,(i1,eq_i1,i1_bl_i1_al )]
*)
let list_id l = List.fold_left ( fun a decl -> let s' =
- match get_name decl with
+ match RelDecl.get_name decl with
Name s -> Id.to_string s
| Anonymous -> "A" in
(Id.of_string s',Id.of_string ("eq_"^s'),
@@ -512,7 +513,7 @@ let eqI ind l =
(List.map (fun (_,seq,_,_)-> mkVar seq) list_id ))
and e, eff =
try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff
- with Not_found -> errorlabstrm "AutoIndDecl.eqI"
+ with Not_found -> user_err ~hdr:"AutoIndDecl.eqI"
(str "The boolean equality on " ++ pr_mind (fst ind) ++ str " is needed.");
in (if Array.equal eq_constr eA [||] then e else mkApp(e,eA)), eff
@@ -543,8 +544,8 @@ let compute_bl_goal ind lnamesparrec nparrec =
mkNamedProd seq b a
) bl_input (List.rev list_id) (List.rev eqs_typ) in
List.fold_left (fun a decl -> mkNamedProd
- (match get_name decl with Name s -> s | Anonymous -> Id.of_string "A")
- (get_type decl) a) eq_input lnamesparrec
+ (match RelDecl.get_name decl with Name s -> s | Anonymous -> Id.of_string "A")
+ (RelDecl.get_type decl) a) eq_input lnamesparrec
in
let n = Id.of_string "x" and
m = Id.of_string "y" in
@@ -639,7 +640,7 @@ let side_effect_of_mode = function
let make_bl_scheme mode mind =
let mib = Global.lookup_mind mind in
if not (Int.equal (Array.length mib.mind_packets) 1) then
- errorlabstrm ""
+ user_err
(str "Automatic building of boolean->Leibniz lemmas not supported");
let ind = (mind,0) in
let nparams = mib.mind_nparams in
@@ -686,8 +687,8 @@ let compute_lb_goal ind lnamesparrec nparrec =
mkNamedProd seq b a
) lb_input (List.rev list_id) (List.rev eqs_typ) in
List.fold_left (fun a decl -> mkNamedProd
- (match (get_name decl) with Name s -> s | Anonymous -> Id.of_string "A")
- (get_type decl) a) eq_input lnamesparrec
+ (match (RelDecl.get_name decl) with Name s -> s | Anonymous -> Id.of_string "A")
+ (RelDecl.get_type decl) a) eq_input lnamesparrec
in
let n = Id.of_string "x" and
m = Id.of_string "y" in
@@ -762,7 +763,7 @@ let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined")
let make_lb_scheme mode mind =
let mib = Global.lookup_mind mind in
if not (Int.equal (Array.length mib.mind_packets) 1) then
- errorlabstrm ""
+ user_err
(str "Automatic building of Leibniz->boolean lemmas not supported");
let ind = (mind,0) in
let nparams = mib.mind_nparams in
@@ -827,8 +828,8 @@ let compute_dec_goal ind lnamesparrec nparrec =
mkNamedProd seq b a
) bl_input (List.rev list_id) (List.rev eqs_typ) in
List.fold_left (fun a decl -> mkNamedProd
- (match get_name decl with Name s -> s | Anonymous -> Id.of_string "A")
- (get_type decl) a) eq_input lnamesparrec
+ (match RelDecl.get_name decl with Name s -> s | Anonymous -> Id.of_string "A")
+ (RelDecl.get_type decl) a) eq_input lnamesparrec
in
let n = Id.of_string "x" and
m = Id.of_string "y" in
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 6d53ec9d8b..0dc7990143 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -98,7 +98,7 @@ let class_of_global = function
| IndRef sp -> CL_IND sp
| VarRef id -> CL_SECVAR id
| ConstructRef _ as c ->
- errorlabstrm "class_of_global"
+ user_err ~hdr:"class_of_global"
(str "Constructors, such as " ++ Printer.pr_global c ++
str ", cannot be used as a class.")
@@ -177,7 +177,7 @@ let ident_key_of_class = function
(* Identity coercion *)
let error_not_transparent source =
- errorlabstrm "build_id_coercion"
+ user_err ~hdr:"build_id_coercion"
(pr_class source ++ str " must be a transparent constant.")
let build_id_coercion idf_opt source poly =
@@ -208,7 +208,7 @@ let build_id_coercion idf_opt source poly =
(Reductionops.is_conv_leq env sigma
(Typing.unsafe_type_of env sigma val_f) typ_f)
then
- errorlabstrm "" (strbrk
+ user_err (strbrk
"Cannot be defined as coercion (maybe a bad number of arguments).")
in
let idf =
@@ -284,7 +284,7 @@ let add_new_coercion_core coef stre poly source target isid =
let try_add_new_coercion_core ref ~local c d e f =
try add_new_coercion_core ref (loc_of_bool local) c d e f
with CoercionError e ->
- errorlabstrm "try_add_new_coercion_core"
+ user_err ~hdr:"try_add_new_coercion_core"
(explain_coercion_error ref e ++ str ".")
let try_add_new_coercion ref ~local poly =
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 1528cbb2f6..6512f3defa 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -22,6 +22,8 @@ open Constrintern
open Constrexpr
open Sigma.Notations
open Context.Rel.Declaration
+
+module RelDecl = Context.Rel.Declaration
(*i*)
open Decl_kinds
@@ -75,8 +77,9 @@ let existing_instance glob g info =
match class_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, "declare_instance",
- Pp.str "Constant does not build instances of a declared type class.")
+ | None -> user_err ~loc:(loc_of_reference g)
+ ~hdr:"declare_instance"
+ (Pp.str "Constant does not build instances of a declared type class.")
let mismatched_params env n m = mismatched_ctx_inst env Parameters n m
let mismatched_props env n m = mismatched_ctx_inst env Properties n m
@@ -86,13 +89,13 @@ let mismatched_props env n m = mismatched_ctx_inst env Properties n m
let type_ctx_instance evars env ctx inst subst =
let rec aux (subst, instctx) l = function
decl :: ctx ->
- let t' = substl subst (get_type decl) in
+ let t' = substl subst (RelDecl.get_type decl) in
let c', l =
match decl with
| LocalAssum _ -> interp_casted_constr_evars env evars (List.hd l) t', List.tl l
| LocalDef (_,b,_) -> substl subst b, l
in
- let d = get_name decl, Some c', t' in
+ let d = RelDecl.get_name decl, Some c', t' in
aux (c' :: subst, d :: instctx) l ctx
| [] -> subst
in aux (subst, []) inst (List.rev ctx)
@@ -165,7 +168,6 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
let cl, u = Typeclasses.typeclass_univ_instance k in
let _, args =
List.fold_right (fun decl (args, args') ->
- let open Context.Rel.Declaration in
match decl with
| LocalAssum _ -> (List.tl args, List.hd args :: args')
| LocalDef (_,b,_) -> (args, substl args' b :: args'))
@@ -178,7 +180,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
Name id ->
let sp = Lib.make_path id in
if Nametab.exists_cci sp then
- errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists.");
+ user_err ~hdr:"new_instance" (Nameops.pr_id id ++ Pp.str " already exists.");
id
| Anonymous ->
let i = Nameops.add_suffix (id_of_class k) "_instance_0" in
@@ -238,7 +240,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
(fun (props, rest) decl ->
if is_local_assum decl then
try
- let is_id (id', _) = match get_name decl, get_id id' with
+ let is_id (id', _) = match RelDecl.get_name decl, get_id id' with
| Name id, (_, id') -> Id.equal id id'
| Anonymous, _ -> false
in
@@ -356,7 +358,7 @@ let named_of_rel_context l =
let acc, ctx =
List.fold_right
(fun decl (subst, ctx) ->
- let id = match get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in
+ let id = match RelDecl.get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in
let d = match decl with
| LocalAssum (_,t) -> id, None, substl subst t
| LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 7ffe680e5e..a8cd52ae8a 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -39,6 +39,8 @@ open Sigma.Notations
open Context.Rel.Declaration
open Entries
+module RelDecl = Context.Rel.Declaration
+
let do_universe poly l = Declare.do_universe poly l
let do_constraint poly l = Declare.do_constraint poly l
@@ -57,8 +59,8 @@ let rec complete_conclusion a cs = function
| CHole (loc, k, _, _) ->
let (has_no_args,name,params) = a in
if not has_no_args then
- user_err_loc (loc,"",
- strbrk"Cannot infer the non constant arguments of the conclusion of "
+ 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)
@@ -330,7 +332,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 (loc, "", msg)
+ user_err ~loc msg
| _ -> ()
in
do_assumptions_bound_univs coe kind nl id (Some pl) c
@@ -342,7 +344,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 (loc, "", msg)
+ user_err ~loc msg
in
(coe, (List.map map idl, c))
in
@@ -438,7 +440,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 (Reduction.is_arity env 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
t, pseudo_poly, impls
@@ -457,7 +459,7 @@ let sign_level env evd sign =
| LocalDef _ -> lev, push_rel d env
| LocalAssum _ ->
let s = destSort (Reduction.whd_all env
- (nf_evar evd (Retyping.get_type_of env evd (get_type d))))
+ (nf_evar evd (Retyping.get_type_of env evd (RelDecl.get_type d))))
in
let u = univ_of_sort s in
(Univ.sup u lev, push_rel d env))
@@ -553,7 +555,7 @@ let check_named (loc, na) = match na with
| Name _ -> ()
| Anonymous ->
let msg = str "Parameters must be named." in
- user_err_loc (loc, "", msg)
+ user_err ~loc msg
let check_param = function
@@ -576,7 +578,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 (fun decl -> out_name (get_name decl)) assums in
+ let params = List.map (RelDecl.get_name %> out_name) assums in
(* Interpret the arities *)
let arities = List.map (interp_ind_arity env_params evdref) indl in
@@ -909,8 +911,8 @@ let rec telescope = function
let ty, tys, (k, constr) =
List.fold_left
(fun (ty, tys, (k, constr)) decl ->
- let t = get_type decl in
- let pred = mkLambda (get_name decl, t, ty) in
+ 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 intro = Universes.constr_of_global (Lazy.force sigT).intro in
let sigty = mkApp (ty, [|t; pred|]) in
@@ -920,7 +922,7 @@ let rec telescope = function
in
let (last, subst) = List.fold_right2
(fun pred decl (prev, subst) ->
- let t = get_type decl in
+ let t = RelDecl.get_type decl in
let p1 = Universes.constr_of_global (Lazy.force sigT).proj1 in
let p2 = Universes.constr_of_global (Lazy.force sigT).proj2 in
let proj1 = applistc p1 [t; pred; prev] in
@@ -954,9 +956,9 @@ 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,
- "Command.build_wellfounded",
- Printer.pr_constr_env env !evdref rel ++ str " is not an homogeneous binary relation.")
+ user_err ~loc:(constr_loc r)
+ ~hdr:"Command.build_wellfounded"
+ (Printer.pr_constr_env env !evdref rel ++ str " is not an homogeneous binary relation.")
in
try
let ctx, ar = Reductionops.splay_prod_n env !evdref 2 relty in
@@ -1133,7 +1135,7 @@ let interp_recursive isfix fixl notations =
let evd, nf = nf_evars_and_universes evd in
let fixdefs = List.map (Option.map nf) fixdefs in
let fixtypes = List.map nf fixtypes in
- let fixctxnames = List.map (fun (_,ctx) -> List.map get_name ctx) fixctxs in
+ let fixctxnames = List.map (fun (_,ctx) -> List.map RelDecl.get_name ctx) fixctxs in
(* Build the fix declaration block *)
(env,rec_sign,all_universes,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxnames fiximps fixannots
@@ -1312,7 +1314,7 @@ let do_program_fixpoint local poly l =
match n with
| Some n -> mkIdentC (snd n)
| None ->
- errorlabstrm "do_program_fixpoint"
+ user_err ~hdr:"do_program_fixpoint"
(str "Recursive argument required for well-founded fixpoints")
in build_wellfounded (id, pl, n, bl, typ, out_def def) poly r recarg ntn
@@ -1326,7 +1328,7 @@ let do_program_fixpoint local poly l =
do_program_recursive local poly fixkind fixl ntns
| _, _ ->
- errorlabstrm "do_program_fixpoint"
+ user_err ~hdr:"do_program_fixpoint"
(str "Well-founded fixpoints not allowed in mutually recursive blocks")
let check_safe () =
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index acbf909cc6..98f60924b9 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -130,13 +130,14 @@ let init_ocaml_path () =
[ "grammar" ]; [ "ide" ]; [ "ltac" ]; ]
let get_compat_version = function
- | "8.6" -> Flags.Current
+ | "8.7" -> Flags.Current
+ | "8.6" -> Flags.V8_6
| "8.5" -> Flags.V8_5
| "8.4" -> Flags.V8_4
| "8.3" -> Flags.V8_3
| "8.2" -> Flags.V8_2
| ("8.1" | "8.0") as s ->
- CErrors.errorlabstrm "get_compat_version"
+ CErrors.user_err ~hdr:"get_compat_version"
(str "Compatibility with version " ++ str s ++ str " not supported.")
- | s -> CErrors.errorlabstrm "get_compat_version"
+ | s -> CErrors.user_err ~hdr:"get_compat_version"
(str "Unknown compatibility version \"" ++ str s ++ str "\".")
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index f98505c362..891662b93a 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -25,6 +25,8 @@ open Printer
open Evd
open Context.Rel.Declaration
+module RelDecl = Context.Rel.Declaration
+
(* This simplifies the typing context of Cases clauses *)
(* hope it does not disturb other typing contexts *)
let contract env lc =
@@ -35,13 +37,10 @@ let contract env lc =
l := (Vars.substl !l c') :: !l;
env
| _ ->
- let t' = Vars.substl !l (get_type decl) in
- let c' = Option.map (Vars.substl !l) (get_value decl) in
- let na' = named_hd env t' (get_name decl) in
+ let t = Vars.substl !l (RelDecl.get_type decl) in
+ let decl = decl |> RelDecl.map_name (named_hd env t) |> RelDecl.map_value (Vars.substl !l) |> RelDecl.set_type t in
l := (mkRel 1) :: List.map (Vars.lift 1) !l;
- match c' with
- | None -> push_rel (LocalAssum (na',t')) env
- | Some c' -> push_rel (LocalDef (na',c',t')) env
+ push_rel decl env
in
let env = process_rel_context contract_context env in
(env, List.map (Vars.substl !l) lc)
@@ -149,7 +148,7 @@ let pr_explicit env sigma t1 t2 = pr_explicit_aux env sigma t1 t2 explicit_flags
let pr_db env i =
try
- match lookup_rel i env |> get_name with
+ match env |> lookup_rel i |> get_name with
| Name id -> pr_id id
| Anonymous -> str "<>"
with Not_found -> str "UNBOUND_REL_" ++ int i
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 6d57a21dc4..85d0b6194c 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -87,7 +87,7 @@ let declare_scheme_object s aux f =
try
let _ = Hashtbl.find scheme_object_table key in
(* let aux_msg = if aux="" then "" else " (with key "^aux^")" in*)
- errorlabstrm "IndTables.declare_scheme_object"
+ user_err ~hdr:"IndTables.declare_scheme_object"
(str "Scheme object " ++ str key ++ str " already declared.")
with Not_found ->
Hashtbl.add scheme_object_table key (s,f);
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index e8ea617f45..48521a8e5d 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -193,7 +193,7 @@ let try_declare_scheme what f internal names kn =
in
match msg with
| None -> ()
- | Some msg -> iraise (UserError ("", msg), snd e)
+ | Some msg -> iraise (UserError (None, msg), snd e)
let beq_scheme_msg mind =
let mib = Global.lookup_mind mind in
diff --git a/toplevel/locality.ml b/toplevel/locality.ml
index 154f787ef4..03640676e6 100644
--- a/toplevel/locality.ml
+++ b/toplevel/locality.ml
@@ -18,7 +18,7 @@ let check_locality locality_flag =
match locality_flag with
| Some b ->
let s = if b then "Local" else "Global" in
- CErrors.errorlabstrm "Locality.check_locality"
+ CErrors.user_err ~hdr:"Locality.check_locality"
(str "This command does not support the \"" ++ str s ++ str "\" prefix.")
| None -> ()
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 008d5cf9f5..f28ef3f650 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -46,12 +46,30 @@ let add_token_obj s = Lib.add_anonymous_leaf (inToken s)
let entry_buf = Buffer.create 64
+type any_entry = AnyEntry : 'a Gram.entry -> any_entry
+
+let grammars : any_entry list String.Map.t ref = ref String.Map.empty
+
+let register_grammar name grams =
+ grammars := String.Map.add name grams !grammars
+
let pr_entry e =
let () = Buffer.clear entry_buf in
let ft = Format.formatter_of_buffer entry_buf in
let () = Gram.entry_print ft e in
str (Buffer.contents entry_buf)
+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."
+ | Some entries ->
+ let pr_one (AnyEntry e) =
+ str "Entry " ++ str (Gram.Entry.name e) ++ str " is" ++ fnl () ++
+ pr_entry e
+ in
+ prlist pr_one entries
+
let pr_grammar = function
| "constr" | "operconstr" | "binder_constr" ->
str "Entry constr is" ++ fnl () ++
@@ -64,15 +82,6 @@ let pr_grammar = function
pr_entry Pcoq.Constr.operconstr
| "pattern" ->
pr_entry Pcoq.Constr.pattern
- | "tactic" ->
- str "Entry tactic_expr is" ++ fnl () ++
- pr_entry Pcoq.Tactic.tactic_expr ++
- str "Entry binder_tactic is" ++ fnl () ++
- pr_entry Pcoq.Tactic.binder_tactic ++
- str "Entry simple_tactic is" ++ fnl () ++
- pr_entry Pcoq.Tactic.simple_tactic ++
- str "Entry tactic_arg is" ++ fnl () ++
- pr_entry Pcoq.Tactic.tactic_arg
| "vernac" ->
str "Entry vernac is" ++ fnl () ++
pr_entry Pcoq.Vernac_.vernac ++
@@ -84,7 +93,7 @@ let pr_grammar = function
pr_entry Pcoq.Vernac_.gallina ++
str "Entry gallina_ext is" ++ fnl () ++
pr_entry Pcoq.Vernac_.gallina_ext
- | _ -> error "Unknown or unprintable grammar entry."
+ | name -> pr_registered_grammar name
(**********************************************************************)
(* Parse a format (every terminal starting with a letter or a single
@@ -238,7 +247,7 @@ let rec find_pattern nt xl = function
| _, Break s :: _ | Break s :: _, _ ->
error ("A break occurs on one side of \"..\" but not on the other side.")
| _, Terminal s :: _ | Terminal s :: _, _ ->
- errorlabstrm "Metasyntax.find_pattern"
+ 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
@@ -300,7 +309,7 @@ let rec get_notation_vars = function
let vars = get_notation_vars sl in
if Id.equal id ldots_var then vars else
if Id.List.mem id vars then
- errorlabstrm "Metasyntax.get_notation_vars"
+ user_err ~hdr:"Metasyntax.get_notation_vars"
(str "Variable " ++ pr_id id ++ str " occurs more than once.")
else
id::vars
@@ -314,7 +323,7 @@ let analyze_notation_tokens l =
recvars, List.subtract Id.equal vars (List.map snd recvars), l
let error_not_same_scope x y =
- errorlabstrm "Metasyntax.error_not_name_scope"
+ user_err ~hdr:"Metasyntax.error_not_name_scope"
(str "Variables " ++ pr_id x ++ str " and " ++ pr_id y ++ str " must be in the same scope.")
(**********************************************************************)
@@ -390,7 +399,7 @@ let check_open_binder isopen sl m =
| _ -> assert false
in
if isopen && not (List.is_empty sl) then
- errorlabstrm "" (str "as " ++ pr_id m ++
+ user_err (str "as " ++ pr_id m ++
str " is a non-closed binder, no such \"" ++
prlist_with_sep spc pr_token sl
++ strbrk "\" is allowed to occur.")
@@ -661,7 +670,7 @@ let pr_level ntn (from,args) =
prlist_with_sep pr_comma (pr_arg_level from) args
let error_incompatible_level ntn oldprec prec =
- errorlabstrm ""
+ user_err
(str "Notation " ++ str ntn ++ str " is already defined" ++ spc() ++
pr_level ntn oldprec ++
spc() ++ str "while it is now required to be" ++ spc() ++
@@ -739,7 +748,7 @@ let interp_modifiers modl =
| SetEntryType (s,typ) :: l ->
let id = Id.of_string s in
if Id.List.mem_assoc id etyps then
- errorlabstrm "Metasyntax.interp_modifiers"
+ user_err ~hdr:"Metasyntax.interp_modifiers"
(str s ++ str " is already assigned to an entry or constr level.");
interp assoc level ((id,typ)::etyps) format extra l
| SetItemLevel ([],n) :: l ->
@@ -747,7 +756,7 @@ let interp_modifiers modl =
| SetItemLevel (s::idl,n) :: l ->
let id = Id.of_string s in
if Id.List.mem_assoc id etyps then
- errorlabstrm "Metasyntax.interp_modifiers"
+ user_err ~hdr:"Metasyntax.interp_modifiers"
(str s ++ str " is already assigned to an entry or constr level.");
let typ = ETConstr (n,()) in
interp assoc level ((id,typ)::etyps) format extra (SetItemLevel (idl,n)::l)
@@ -781,7 +790,7 @@ let check_infix_modifiers modifiers =
let check_useless_entry_types recvars mainvars etyps =
let vars = let (l1,l2) = List.split recvars in l1@l2@mainvars in
match List.filter (fun (x,etyp) -> not (List.mem x vars)) etyps with
- | (x,_)::_ -> errorlabstrm "Metasyntax.check_useless_entry_types"
+ | (x,_)::_ -> user_err ~hdr:"Metasyntax.check_useless_entry_types"
(pr_id x ++ str " is unbound in the notation.")
| _ -> ()
@@ -829,7 +838,7 @@ let join_auxiliary_recursive_types recvars etyps =
| None, Some ytyp -> (x,ytyp)::typs
| Some xtyp, Some ytyp when Pervasives.(=) xtyp ytyp -> typs (* FIXME *)
| Some xtyp, Some ytyp ->
- errorlabstrm ""
+ user_err
(strbrk "In " ++ pr_id x ++ str " .. " ++ pr_id y ++
strbrk ", both ends have incompatible types."))
recvars etyps
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 085cc87c8b..57c1204022 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Names
-open Tacexpr
open Vernacexpr
open Notation
open Constrexpr
@@ -55,6 +54,10 @@ val add_syntactic_definition : Id.t -> Id.t list * constr_expr ->
val pr_grammar : string -> Pp.std_ppcmds
+type any_entry = AnyEntry : 'a Pcoq.Gram.entry -> any_entry
+
+val register_grammar : string -> any_entry list -> unit
+
val check_infix_modifiers : syntax_modifier list -> unit
val with_syntax_protection : ('a -> 'b) -> 'a -> 'b
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index b6690fe47b..2396cf04a4 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -124,13 +124,13 @@ let ml_load s =
| (UserError _ | Failure _ | Not_found as u) -> Exninfo.iraise (u, snd e)
| exc ->
let msg = report_on_load_obj_error exc in
- errorlabstrm "Mltop.load_object" (str"Cannot link ml-object " ++
+ user_err ~hdr:"Mltop.load_object" (str"Cannot link ml-object " ++
str s ++ str" to Coq code (" ++ msg ++ str ")."))
| WithoutTop ->
try
Dynlink.loadfile s; s
with Dynlink.Error a ->
- errorlabstrm "Mltop.load_object"
+ user_err ~hdr:"Mltop.load_object"
(strbrk "while loading " ++ str s ++
strbrk ": " ++ str (Dynlink.error_message a))
@@ -151,7 +151,7 @@ let dir_ml_use s =
if Dynlink.is_native then " Loading ML code works only in bytecode."
else ""
in
- errorlabstrm "Mltop.dir_ml_use" (str "Could not load ML code." ++ str moreinfo)
+ user_err ~hdr:"Mltop.dir_ml_use" (str "Could not load ML code." ++ str moreinfo)
(* Adds a path to the ML paths *)
let add_ml_dir s =
@@ -226,7 +226,7 @@ let get_ml_object_suffix name =
let file_of_name name =
let suffix = get_ml_object_suffix name in
let fail s =
- errorlabstrm "Mltop.load_object"
+ user_err ~hdr:"Mltop.load_object"
(str"File not found on loadpath : " ++ str s ++ str"\n" ++
str"Loadpath: " ++ str(String.concat ":" !coq_mlpath_copy)) in
if not (Filename.is_relative name) then
@@ -360,7 +360,7 @@ let trigger_ml_object verb cache reinit ?path name =
add_loaded_module name (known_module_path name);
if cache then perform_cache_obj name
end else if not has_dynlink then
- errorlabstrm "Mltop.trigger_ml_object"
+ user_err ~hdr:"Mltop.trigger_ml_object"
(str "Dynamic link not supported (module " ++ str name ++ str ")")
else begin
let file = file_of_name (Option.default name path) in
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 29d7457321..9ada043171 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -20,6 +20,8 @@ open Pp
open CErrors
open Util
+module NamedDecl = Context.Named.Declaration
+
let declare_fix_ref = ref (fun ?opaque _ _ _ _ _ _ -> assert false)
let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false)
@@ -34,7 +36,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 =
@@ -51,7 +53,6 @@ type oblinfo =
where n binders were passed through. *)
let subst_evar_constr evs n idf t =
- let open Context.Named.Declaration in
let seen = ref Int.Set.empty in
let transparent = ref Id.Set.empty in
let evar_info id = List.assoc_f Evar.equal id evs in
@@ -74,6 +75,7 @@ let subst_evar_constr evs n idf t =
in
let args =
let rec aux hyps args acc =
+ let open Context.Named.Declaration in
match hyps, args with
(LocalAssum _ :: tlh), (c :: tla) ->
aux tlh tla ((substrec (depth, fixrels) c) :: acc)
@@ -116,9 +118,9 @@ let etype_of_evar evs hyps concl =
let open Context.Named.Declaration in
let rec aux acc n = function
decl :: tl ->
- let t', s, trans = subst_evar_constr evs n mkVar (get_type decl) in
+ let t', s, trans = subst_evar_constr evs n mkVar (NamedDecl.get_type decl) in
let t'' = subst_vars acc 0 t' in
- let rest, s', trans' = aux (get_id decl :: acc) (succ n) tl in
+ let rest, s', trans' = aux (NamedDecl.get_id decl :: acc) (succ n) tl in
let s' = Int.Set.union s s' in
let trans' = Id.Set.union trans trans' in
(match decl with
@@ -258,7 +260,7 @@ let safe_init_constant md name () =
Coqlib.gen_constant "Obligations" md name
let hide_obligation = safe_init_constant tactics_module "obligation"
-let pperror cmd = CErrors.errorlabstrm "Program" cmd
+let pperror cmd = CErrors.user_err ~hdr:"Program" cmd
let error s = pperror (str s)
let reduce c =
@@ -394,11 +396,11 @@ let subst_deps expand obls deps t =
(Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t)
let rec prod_app t n =
- match kind_of_term (strip_outer_cast t) with
+ match kind_of_term (Termops.strip_outer_cast t) with
| Prod (_,_,b) -> subst1 n b
| LetIn (_, b, t, b') -> prod_app (subst1 b b') n
| _ ->
- errorlabstrm "prod_app"
+ user_err ~hdr:"prod_app"
(str"Needed a product, but didn't find one" ++ fnl ())
@@ -444,7 +446,7 @@ let from_prg : program_info ProgMap.t ref =
let close sec =
if not (ProgMap.is_empty !from_prg) then
let keys = map_keys !from_prg in
- errorlabstrm "Program"
+ user_err ~hdr:"Program"
(str "Unsolved obligations when closing " ++ str sec ++ str":" ++ spc () ++
prlist_with_sep spc (fun x -> Nameops.pr_id x) keys ++
(str (if Int.equal (List.length keys) 1 then " has " else " have ") ++
@@ -598,7 +600,6 @@ let decompose_lam_prod c ty =
in aux Context.Rel.empty c ty
let shrink_body c ty =
- let open Context.Rel.Declaration in
let ctx, b, ty =
match ty with
| None ->
@@ -613,6 +614,7 @@ let shrink_body c ty =
if noccurn 1 b && Option.cata (noccurn 1) true ty then
subst1 mkProp b, Option.map (subst1 mkProp) ty, succ i, args
else
+ let open Context.Rel.Declaration in
let args = if is_local_assum decl then mkRel i :: args else args in
mkLambda_or_LetIn decl b, Option.map (mkProd_or_LetIn decl) ty,
succ i, args)
@@ -718,7 +720,7 @@ let get_prog name =
let progs = Id.Set.elements (ProgMap.domain prg_infos) in
let prog = List.hd progs in
let progs = prlist_with_sep pr_comma Nameops.pr_id progs in
- errorlabstrm ""
+ user_err
(str "More than one program with unsolved obligations: " ++ progs
++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Nameops.pr_id prog ++ str "\""))
@@ -985,7 +987,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, "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/toplevel/obligations.mli b/toplevel/obligations.mli
index 69d2069616..80b6891447 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -87,9 +87,9 @@ val add_mutual_definitions :
fixpoint_kind -> unit
val obligation : int * Names.Id.t option * Constrexpr.constr_expr option ->
- Tacexpr.raw_tactic_expr option -> unit
+ Genarg.glob_generic_argument option -> unit
-val next_obligation : Names.Id.t option -> Tacexpr.raw_tactic_expr option -> unit
+val next_obligation : Names.Id.t option -> Genarg.glob_generic_argument option -> unit
val solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> progress
(* Number of remaining obligations to be solved for this program *)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index ef09f6fa54..76de9d7adb 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -27,6 +27,8 @@ open Goptions
open Sigma.Notations
open Context.Rel.Declaration
+module RelDecl = Context.Rel.Declaration
+
(********** definition d'un record (structure) **************)
(** Flag governing use of primitive projections. Disabled by default. *)
@@ -82,7 +84,7 @@ let compute_constructor_level evars env l =
List.fold_right (fun d (env, univ) ->
let univ =
if is_local_assum d then
- let s = Retyping.get_sort_of env evars (get_type d) in
+ let s = Retyping.get_sort_of env evars (RelDecl.get_type d) in
Univ.sup (univ_of_sort s) univ
else univ
in (push_rel d env, univ))
@@ -102,7 +104,7 @@ 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 (loc, "record", str "Record parameters must be named")
+ user_err ~loc ~hdr:"record" (str "Record parameters must be named")
| _ -> ()
in
List.iter
@@ -127,7 +129,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
@@ -167,7 +169,7 @@ let typecheck_params_and_fields def id pl t ps nots fs =
Evd.universe_context ?names:pl evars, nf arity, template, imps, newps, impls, newfs
let degenerate_decl decl =
- let id = match get_name decl with
+ let id = match RelDecl.get_name decl with
| Name id -> id
| Anonymous -> anomaly (Pp.str "Unnamed record variable") in
match decl with
@@ -208,7 +210,7 @@ let warning_or_error coe indsp err =
| _ ->
(pr_id fi ++ strbrk " cannot be defined because it is not typable.")
in
- if coe then errorlabstrm "structure" st;
+ if coe then user_err ~hdr:"structure" st;
Flags.if_verbose Feedback.msg_info (hov 0 st)
type field_status =
@@ -235,7 +237,7 @@ let subst_projection fid l c =
| Projection t -> lift depth t
| NoProjection (Name id) -> bad_projs := id :: !bad_projs; mkRel k
| NoProjection Anonymous ->
- errorlabstrm "" (str "Field " ++ pr_id fid ++
+ user_err (str "Field " ++ pr_id fid ++
str " depends on the " ++ pr_nth (k-depth-1) ++ str
" field which has no name.")
else
@@ -288,8 +290,8 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
let (_,_,kinds,sp_projs,_) =
List.fold_left3
(fun (nfi,i,kinds,sp_projs,subst) coe decl impls ->
- let fi = get_name decl in
- let ti = get_type decl in
+ let fi = RelDecl.get_name decl in
+ let ti = RelDecl.get_type decl in
let (sp_projs,i,subst) =
match fi with
| Anonymous ->
@@ -362,17 +364,17 @@ let structure_signature ctx =
| [decl] ->
let env = Environ.empty_named_context_val in
let evm = Sigma.Unsafe.of_evar_map evm in
- let Sigma (_, evm, _) = Evarutil.new_pure_evar env evm (get_type decl) in
+ let Sigma (_, evm, _) = Evarutil.new_pure_evar env evm (RelDecl.get_type decl) in
let evm = Sigma.to_evar_map evm in
evm
| decl::tl ->
let env = Environ.empty_named_context_val in
let evm = Sigma.Unsafe.of_evar_map evm in
- let Sigma (ev, evm, _) = Evarutil.new_pure_evar env evm (get_type decl) in
+ let Sigma (ev, evm, _) = Evarutil.new_pure_evar env evm (RelDecl.get_type decl) in
let evm = Sigma.to_evar_map evm in
let new_tl = Util.List.map_i
(fun pos decl ->
- map_type (fun t -> Termops.replace_term (mkRel pos) (mkEvar(ev,[||])) t) decl) 1 tl in
+ RelDecl.map_type (fun t -> Termops.replace_term (mkRel pos) (mkEvar(ev,[||])) t) decl) 1 tl in
deps_to_evar evm new_tl in
deps_to_evar Evd.empty (List.rev ctx)
@@ -422,7 +424,7 @@ let implicits_of_context ctx =
| Name n -> Some n
| Anonymous -> None
in ExplByPos (i, explname), (true, true, true))
- 1 (List.rev (Anonymous :: (List.map get_name ctx)))
+ 1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
let declare_class finite def poly ctx id idbuild paramimpls params arity
template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign =
@@ -476,13 +478,13 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity
if b then Backward, pri else Forward, pri) coe)
coers priorities
in
- let l = List.map3 (fun decl b y -> get_name decl, b, y)
+ let l = List.map3 (fun decl b y -> RelDecl.get_name decl, b, y)
(List.rev fields) coers (Recordops.lookup_projections ind)
in IndRef ind, l
in
let ctx_context =
List.map (fun decl ->
- match Typeclasses.class_of_constr (get_type decl) with
+ match Typeclasses.class_of_constr (RelDecl.get_type decl) with
| Some (_, ((cl,_), _)) -> Some (cl.cl_impl, true)
| None -> None)
params, params
@@ -533,8 +535,8 @@ let declare_existing_class g =
match g with
| ConstRef x -> add_constant_class x
| IndRef x -> add_inductive_class x
- | _ -> user_err_loc (Loc.dummy_loc, "declare_existing_class",
- Pp.str"Unsupported class type, only constants and inductives are allowed")
+ | _ -> user_err ~hdr:"declare_existing_class"
+ (Pp.str"Unsupported class type, only constants and inductives are allowed")
open Vernacexpr
diff --git a/toplevel/search.ml b/toplevel/search.ml
index ff3c7a4f42..d319b24199 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -20,6 +20,8 @@ open Globnames
open Nametab
open Goptions
+module NamedDecl = Context.Named.Declaration
+
type filter_function = global_reference -> env -> constr -> bool
type display_function = global_reference -> env -> constr -> unit
@@ -57,8 +59,7 @@ let iter_constructors indsp u fn env nconstr =
done
let iter_named_context_name_type f =
- let open Context.Named.Declaration in
- List.iter (fun decl -> f (get_id decl) (get_type decl))
+ List.iter (fun decl -> f (NamedDecl.get_id decl) (NamedDecl.get_type decl))
(* General search over hypothesis of a goal *)
let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) =
@@ -70,13 +71,12 @@ let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) =
(* General search over declarations *)
let iter_declarations (fn : global_reference -> env -> constr -> unit) =
- let open Context.Named.Declaration in
let env = Global.env () in
let iter_obj (sp, kn) lobj = match object_tag lobj with
| "VARIABLE" ->
begin try
let decl = Global.lookup_named (basename sp) in
- fn (VarRef (get_id decl)) env (get_type decl)
+ fn (VarRef (NamedDecl.get_id decl)) env (NamedDecl.get_type decl)
with Not_found -> (* we are in a section *) () end
| "CONSTANT" ->
let cst = Global.constant_of_delta_kn kn in
@@ -112,7 +112,7 @@ let generic_search glnumopt fn =
(** This function tries to see whether the conclusion matches a pattern. *)
(** FIXME: this is quite dummy, we may find a more efficient algorithm. *)
let rec pattern_filter pat ref env typ =
- let typ = strip_outer_cast typ in
+ let typ = Termops.strip_outer_cast typ in
if Constr_matching.is_matching env Evd.empty pat typ then true
else match kind_of_term typ with
| Prod (_, _, typ)
@@ -120,7 +120,7 @@ let rec pattern_filter pat ref env typ =
| _ -> false
let rec head_filter pat ref env typ =
- let typ = strip_outer_cast typ in
+ let typ = Termops.strip_outer_cast typ in
if Constr_matching.is_matching_head env Evd.empty pat typ then true
else match kind_of_term typ with
| Prod (_, _, typ)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index bfdae85d50..0e72a044c1 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -18,7 +18,7 @@ open Vernacexpr
Use the module Coqtoplevel, which catches these exceptions
(the exceptions are explained only at the toplevel). *)
-let user_error loc s = CErrors.user_err_loc (loc,"_",str s)
+let user_error loc s = CErrors.user_err ~loc (str s)
(* Navigation commands are allowed in a coqtop session but not in a .v file *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 41ee165ff8..8ce13c69af 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -33,6 +33,8 @@ open Misctypes
open Locality
open Sigma.Notations
+module NamedDecl = Context.Named.Declaration
+
(** TODO: make this function independent of Ltac *)
let (f_interp_redexp, interp_redexp_hook) = Hook.make ()
@@ -105,7 +107,7 @@ let show_intro all =
let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in
if not (List.is_empty gls) then begin
let gl = {Evd.it=List.hd gls ; sigma = sigma; } in
- let l,_= decompose_prod_assum (strip_outer_cast (pf_concl gl)) in
+ let l,_= decompose_prod_assum (Termops.strip_outer_cast (pf_concl gl)) in
if all then
let lid = Tactics.find_intro_names l gl in
Feedback.msg_notice (hov 0 (prlist_with_sep spc pr_id lid))
@@ -383,9 +385,9 @@ let err_unmapped_library loc ?from qid =
| Some from ->
str " and prefix " ++ pr_dirpath from ++ str "."
in
- user_err_loc
- (loc,"locate_library",
- strbrk "Cannot find a physical path bound to logical path matching suffix " ++
+ 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 =
@@ -394,9 +396,8 @@ let err_notfound_library loc ?from qid =
| Some from ->
str " with prefix " ++ pr_dirpath from ++ str "."
in
- user_err_loc
- (loc,"locate_library",
- strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix)
+ 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
@@ -407,13 +408,13 @@ let print_located_library r =
let smart_global r =
let gr = Smartlocate.smart_global r in
- Dumpglob.add_glob (Constrarg.loc_of_or_by_notation loc_of_reference r) gr;
+ Dumpglob.add_glob (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 (Constrarg.loc_of_or_by_notation loc_of_reference r) gr
+ Dumpglob.add_glob (Stdarg.loc_of_or_by_notation loc_of_reference r) gr
with e when CErrors.noncritical e -> ()
(**********)
(* Syntax *)
@@ -507,7 +508,7 @@ let vernac_start_proof locality p kind l lettop =
| None -> ()) l;
if not(refining ()) then
if lettop then
- errorlabstrm "Vernacentries.StartProof"
+ user_err ~hdr:"Vernacentries.StartProof"
(str "Let declarations can only be used in proof editing mode.");
start_proof_and_print (local, p, Proof kind) l no_hook
@@ -628,15 +629,15 @@ let vernac_combined_scheme lid l =
let vernac_universe loc poly l =
if poly && not (Lib.sections_are_opened ()) then
- user_err_loc (loc, "vernac_universe",
- str"Polymorphic universes can only be declared inside sections, " ++
+ 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 (loc, "vernac_constraint",
- str"Polymorphic universe constraints can only be declared"
+ 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
@@ -863,23 +864,23 @@ 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 _, tac = Genintern.generic_intern env tac in
if not (refining ()) then
error "Unknown command of the non proof-editing mode.";
- match tac with
- | Tacexpr.TacId [] -> ()
- | _ -> set_end_tac tac
+ set_end_tac tac
(* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
let vernac_set_used_variables e =
- let open Context.Named.Declaration in
let env = Global.env () in
let tys =
List.map snd (Proof.initial_goals (Proof_global.give_me_the_proof ())) in
let l = Proof_using.process_expr env e tys in
let vars = Environ.named_context env in
List.iter (fun id ->
- if not (List.exists (Id.equal id % get_id) vars) then
- errorlabstrm "vernac_set_used_variables"
+ if not (List.exists (NamedDecl.get_id %> Id.equal id) vars) then
+ user_err ~hdr:"vernac_set_used_variables"
(str "Unknown variable: " ++ pr_id id))
l;
let _, to_clear = set_used_variables l in
@@ -1021,12 +1022,12 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
(* Checks *)
let err_extra_args names =
- errorlabstrm "vernac_declare_arguments"
+ user_err ~hdr:"vernac_declare_arguments"
(strbrk "Extra arguments: " ++
prlist_with_sep pr_comma pr_name names ++ str ".")
in
let err_missing_args names =
- errorlabstrm "vernac_declare_arguments"
+ user_err ~hdr:"vernac_declare_arguments"
(strbrk "The following arguments are not declared: " ++
prlist_with_sep pr_comma pr_name names ++ str ".")
in
@@ -1107,7 +1108,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
let renaming_specified = Option.has_some !example_renaming in
if !rename_flag_required && not rename_flag then
- errorlabstrm "vernac_declare_arguments"
+ user_err ~hdr:"vernac_declare_arguments"
(strbrk "To rename arguments the \"rename\" flag must be specified."
++ spc () ++
match !example_renaming with
@@ -1121,7 +1122,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
in
if not (List.is_empty duplicate_names) then begin
let duplicates = prlist_with_sep pr_comma pr_name duplicate_names in
- errorlabstrm "_" (strbrk "Some argument names are duplicated: " ++ duplicates)
+ user_err (strbrk "Some argument names are duplicated: " ++ duplicates)
end;
(* Parts of this code are overly complicated because the implicit arguments
@@ -1148,7 +1149,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
(* With the current impargs API, it is impossible to make an originally
anonymous argument implicit *)
| Anonymous :: _, (name, _) :: _ ->
- errorlabstrm "vernac_declare_arguments"
+ user_err ~hdr:"vernac_declare_arguments"
(strbrk"Argument "++ pr_name name ++
strbrk " cannot be declared implicit.")
@@ -1215,7 +1216,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
Reductionops.ReductionBehaviour.set
(make_section_locality locality) c
(rargs, Option.default ~-1 nargs_for_red, red_flags)
- | _ -> errorlabstrm ""
+ | _ -> user_err
(strbrk "Modifiers of the behavior of the simpl tactic "++
strbrk "are relevant for constants only.")
end;
@@ -1639,7 +1640,7 @@ let print_about_hyp_globs ref_or_by_not glnumopt =
| Some n,AN (Ident (_loc,id)) -> (* goal number given, catch if wong *)
(try get_nth_goal n,id
with
- Failure _ -> errorlabstrm "print_about_hyp_globs"
+ Failure _ -> user_err ~hdr:"print_about_hyp_globs"
(str "No such goal: " ++ int n ++ str "."))
| _ , _ -> raise NoHyp in
let hyps = pf_hyps gl in
@@ -1647,7 +1648,7 @@ let print_about_hyp_globs ref_or_by_not glnumopt =
let natureofid = match decl with
| LocalAssum _ -> "Hypothesis"
| LocalDef (_,bdy,_) ->"Constant (let in)" in
- v 0 (pr_id id ++ str":" ++ pr_constr (get_type decl) ++ fnl() ++ fnl()
+ v 0 (pr_id id ++ str":" ++ pr_constr (NamedDecl.get_type decl) ++ fnl() ++ fnl()
++ str natureofid ++ str " of the goal context.")
with (* fallback to globals *)
| NoHyp | Not_found -> print_about ref_or_by_not
@@ -1715,8 +1716,8 @@ let global_module r =
let (loc,qid) = qualid_of_reference r in
try Nametab.full_name_module qid
with Not_found ->
- user_err_loc (loc, "global_module",
- str "Module/section " ++ pr_qualid qid ++ str " not found.")
+ user_err ~loc ~hdr:"global_module"
+ (str "Module/section " ++ pr_qualid qid ++ str " not found.")
let interp_search_restriction = function
| SearchOutside l -> (List.map global_module l, true)
@@ -1738,7 +1739,7 @@ let interp_search_about_item env =
(fun _ -> true) s sc in
GlobSearchSubPattern (Pattern.PRef ref)
with UserError _ ->
- errorlabstrm "interp_search_about_item"
+ user_err ~hdr:"interp_search_about_item"
(str "Unable to interp \"" ++ str s ++ str "\" either as a reference or as an identifier component")
(* 05f22a5d6d5b8e3e80f1a37321708ce401834430 introduced the
@@ -2054,12 +2055,12 @@ let interp ?proof ~loc locality poly c =
| VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n")
(* The STM should handle that, but LOAD bypasses the STM... *)
- | VernacAbort id -> CErrors.errorlabstrm "" (str "Abort cannot be used through the Load command")
- | VernacAbortAll -> CErrors.errorlabstrm "" (str "AbortAll cannot be used through the Load command")
- | VernacRestart -> CErrors.errorlabstrm "" (str "Restart cannot be used through the Load command")
- | VernacUndo _ -> CErrors.errorlabstrm "" (str "Undo cannot be used through the Load command")
- | VernacUndoTo _ -> CErrors.errorlabstrm "" (str "UndoTo cannot be used through the Load command")
- | VernacBacktrack _ -> CErrors.errorlabstrm "" (str "Backtrack cannot be used through the Load command")
+ | VernacAbort id -> CErrors.user_err (str "Abort cannot be used through the Load command")
+ | VernacAbortAll -> CErrors.user_err (str "AbortAll cannot be used through the Load command")
+ | VernacRestart -> CErrors.user_err (str "Restart cannot be used through the Load command")
+ | VernacUndo _ -> CErrors.user_err (str "Undo cannot be used through the Load command")
+ | VernacUndoTo _ -> CErrors.user_err (str "UndoTo cannot be used through the Load command")
+ | VernacBacktrack _ -> CErrors.user_err (str "Backtrack cannot be used through the Load command")
(* Proof management *)
| VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t,None)] false
@@ -2191,7 +2192,7 @@ let with_fail b f =
let (e, _) = CErrors.push e in
match e with
| HasNotFailed ->
- errorlabstrm "Fail" (str "The command has not failed!")
+ user_err ~hdr:"Fail" (str "The command has not failed!")
| HasFailed msg ->
if is_verbose () || !test_mode || !ide_slave then Feedback.msg_info
(str "The command has indeed failed with message:" ++ fnl () ++ msg)
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 4e7fa4a087..7cdc8dd064 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -62,5 +62,5 @@ val with_fail : bool -> (unit -> unit) -> unit
val command_focus : unit Proof.focus_kind
-val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Tacexpr.raw_red_expr ->
+val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr ->
Evd.evar_map * Redexpr.red_expr) Hook.t
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index d81e3d6b56..f26ef460dd 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -22,7 +22,7 @@ let vinterp_add depr s f =
try
Hashtbl.add vernac_tab s (depr, f)
with Failure _ ->
- errorlabstrm "vinterp_add"
+ user_err ~hdr:"vinterp_add"
(str"Cannot add the vernac command " ++ str (fst s) ++ str" twice.")
let overwriting_vinterp_add s f =
@@ -37,7 +37,7 @@ let vinterp_map s =
try
Hashtbl.find vernac_tab s
with Failure _ | Not_found ->
- errorlabstrm "Vernac Interpreter"
+ user_err ~hdr:"Vernac Interpreter"
(str"Cannot find vernac command " ++ str (fst s) ++ str".")
let vinterp_init () = Hashtbl.clear vernac_tab
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 12:16:08 +0000