aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.ml22
-rw-r--r--proofs/evar_refiner.ml4
-rw-r--r--proofs/goal.ml7
-rw-r--r--proofs/logic.ml45
-rw-r--r--proofs/pfedit.ml4
-rw-r--r--proofs/pfedit.mli4
-rw-r--r--proofs/proof.ml4
-rw-r--r--proofs/proof_global.ml14
-rw-r--r--proofs/proof_global.mli4
-rw-r--r--proofs/proof_using.ml16
-rw-r--r--proofs/redexpr.ml10
-rw-r--r--proofs/refine.ml4
-rw-r--r--proofs/refiner.ml19
-rw-r--r--proofs/tacmach.ml10
14 files changed, 91 insertions, 76 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 0a90e0dbd3..fad656223a 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -155,7 +155,7 @@ let error_incompatible_inst clenv mv =
let na = meta_name clenv.evd mv in
match na with
Name id ->
- errorlabstrm "clenv_assign"
+ user_err ~hdr:"clenv_assign"
(str "An incompatible instantiation has already been found for " ++
pr_id id)
| _ ->
@@ -417,11 +417,11 @@ let qhyp_eq h1 h2 = match h1, h2 with
let check_bindings bl =
match List.duplicates qhyp_eq (List.map pi2 bl) with
| NamedHyp s :: _ ->
- errorlabstrm ""
+ user_err
(str "The variable " ++ pr_id s ++
str " occurs more than once in binding list.");
| AnonHyp n :: _ ->
- errorlabstrm ""
+ user_err
(str "The position " ++ int n ++
str " occurs more than once in binding list.")
| [] -> ()
@@ -435,7 +435,7 @@ let explain_no_such_bound_variable evd id =
if na != Anonymous then out_name na :: l else l
in
let mvl = List.fold_left fold [] (Evd.meta_list evd) in
- errorlabstrm "Evd.meta_with_name"
+ user_err ~hdr:"Evd.meta_with_name"
(str"No such bound variable " ++ pr_id id ++
(if mvl == [] then str " (no bound variables at all in the expression)."
else
@@ -460,7 +460,7 @@ let meta_with_name evd id =
| ([n],_|_,[n]) ->
n
| _ ->
- errorlabstrm "Evd.meta_with_name"
+ user_err ~hdr:"Evd.meta_with_name"
(str "Binder name \"" ++ pr_id id ++
strbrk "\" occurs more than once in clause.")
@@ -469,12 +469,12 @@ let meta_of_binder clause loc mvs = function
| AnonHyp n ->
try List.nth mvs (n-1)
with (Failure _|Invalid_argument _) ->
- errorlabstrm "" (str "No such binder.")
+ user_err (str "No such binder.")
let error_already_defined b =
match b with
| NamedHyp id ->
- errorlabstrm ""
+ user_err
(str "Binder name \"" ++ pr_id id ++
str"\" already defined with incompatible value.")
| AnonHyp n ->
@@ -527,7 +527,7 @@ let clenv_constrain_last_binding c clenv =
clenv_assign_binding clenv k c
let error_not_right_number_missing_arguments n =
- errorlabstrm ""
+ user_err
(strbrk "Not the right number of missing arguments (expected " ++
int n ++ str ").")
@@ -641,7 +641,7 @@ let explain_no_such_bound_variable holes id =
| [id] -> str "(possible name is: " ++ pr_id id ++ str ")."
| _ -> str "(possible names are: " ++ pr_enum pr_id mvl ++ str ")."
in
- errorlabstrm "" (str "No such bound variable " ++ pr_id id ++ expl)
+ user_err (str "No such bound variable " ++ pr_id id ++ expl)
let evar_with_name holes id =
let map h = match h.hole_name with
@@ -653,7 +653,7 @@ let evar_with_name holes id =
| [] -> explain_no_such_bound_variable holes id
| [h] -> h.hole_evar
| _ ->
- errorlabstrm ""
+ user_err
(str "Binder name \"" ++ pr_id id ++
str "\" occurs more than once in clause.")
@@ -664,7 +664,7 @@ let evar_of_binder holes = function
let h = List.nth holes (pred n) in
h.hole_evar
with e when CErrors.noncritical e ->
- errorlabstrm "" (str "No such binder.")
+ user_err (str "No such binder.")
let define_with_type sigma env ev c =
let t = Retyping.get_type_of env sigma ev in
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 5f0cc73d2c..ff0df9179f 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -54,8 +54,8 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc
with e when CErrors.noncritical e ->
let loc = Glob_ops.loc_of_glob_constr rawc in
- user_err_loc
- (loc,"", str "Instance is not well-typed in the environment of " ++
+ user_err ~loc
+ (str "Instance is not well-typed in the environment of " ++
pr_existential_key sigma evk ++ str ".")
in
define_and_solve_constraints evk typed_c env (evars_reset_evd sigma' sigma)
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 111a947a9c..a141708c2b 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -10,7 +10,8 @@ open Util
open Pp
open Term
open Sigma.Notations
-open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
(* This module implements the abstract interface to goals *)
(* A general invariant of the module, is that a goal whose associated
@@ -77,7 +78,7 @@ module V82 = struct
let evars = Sigma.to_evar_map evars in
let evars = Evd.restore_future_goals evars prev_future_goals prev_principal_goal in
let ctxt = Environ.named_context_of_val hyps in
- let inst = Array.map_of_list (mkVar % get_id) ctxt in
+ let inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in
let ev = Term.mkEvar (evk,inst) in
(evk, ev, evars)
@@ -148,7 +149,7 @@ module V82 = struct
let env = env sigma gl in
let genv = Global.env () in
let is_proof_var decl =
- try ignore (Environ.lookup_named (get_id decl) genv); false
+ try ignore (Environ.lookup_named (NamedDecl.get_id decl) genv); false
with Not_found -> true in
Environ.fold_named_context_reverse (fun t decl ->
if is_proof_var decl then
diff --git a/proofs/logic.ml b/proofs/logic.ml
index aa0b9bac6f..5aba6b614f 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -24,6 +24,8 @@ open Retyping
open Misctypes
open Context.Named.Declaration
+module NamedDecl = Context.Named.Declaration
+
type refiner_error =
(* Errors raised by the refiner *)
@@ -151,7 +153,7 @@ let reorder_context env sign ord =
| top::ord' when mem_q top moved_hyps ->
let ((d,h),mh) = find_q top moved_hyps in
if occur_vars_in_decl env h d then
- errorlabstrm "reorder_context"
+ user_err ~hdr:"reorder_context"
(str "Cannot move declaration " ++ pr_id top ++ spc() ++
str "before " ++
pr_sequence pr_id
@@ -162,7 +164,7 @@ let reorder_context env sign ord =
(match ctxt_head with
| [] -> error_no_such_hypothesis (List.hd ord)
| d :: ctxt ->
- let x = get_id d in
+ let x = NamedDecl.get_id d in
if Id.Set.mem x expected then
step ord (Id.Set.remove x expected)
ctxt (push_item x d moved_hyps) ctxt_tail
@@ -178,11 +180,11 @@ let reorder_val_context env sign ord =
let check_decl_position env sign d =
- let x = get_id d in
+ let x = NamedDecl.get_id d in
let needed = global_vars_set_of_decl env d in
let deps = dependency_closure env (named_context_of_val sign) needed in
if Id.List.mem x deps then
- errorlabstrm "Logic.check_decl_position"
+ user_err ~hdr:"Logic.check_decl_position"
(str "Cannot create self-referring hypothesis " ++ pr_id x);
x::deps
@@ -204,8 +206,8 @@ let move_location_eq m1 m2 = match m1, m2 with
let rec get_hyp_after h = function
| [] -> error_no_such_hypothesis h
| d :: right ->
- if Id.equal (get_id d) h then
- match right with d' ::_ -> MoveBefore (get_id d') | [] -> MoveFirst
+ if Id.equal (NamedDecl.get_id d) h then
+ match right with d' ::_ -> MoveBefore (NamedDecl.get_id d') | [] -> MoveFirst
else
get_hyp_after h right
@@ -213,7 +215,7 @@ let split_sign hfrom hto l =
let rec splitrec left toleft = function
| [] -> error_no_such_hypothesis hfrom
| d :: right ->
- let hyp,_,typ = to_tuple d in
+ let hyp = NamedDecl.get_id d in
if Id.equal hyp hfrom then
(left,right,d, toleft || move_location_eq hto MoveLast)
else
@@ -235,24 +237,24 @@ let move_hyp toleft (left,declfrom,right) hto =
let env = Global.env() in
let test_dep d d2 =
if toleft
- then occur_var_in_decl env (get_id d2) d
- else occur_var_in_decl env (get_id d) d2
+ then occur_var_in_decl env (NamedDecl.get_id d2) d
+ else occur_var_in_decl env (NamedDecl.get_id d) d2
in
let rec moverec first middle = function
| [] ->
if match hto with MoveFirst | MoveLast -> false | _ -> true then
error_no_such_hypothesis (hyp_of_move_location hto);
List.rev first @ List.rev middle
- | d :: _ as right when move_location_eq hto (MoveBefore (get_id d)) ->
+ | d :: _ as right when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) ->
List.rev first @ List.rev middle @ right
| d :: right ->
- let hyp = get_id d in
+ let hyp = NamedDecl.get_id d in
let (first',middle') =
if List.exists (test_dep d) middle then
if not (move_location_eq hto (MoveAfter hyp)) then
(first, d::middle)
else
- errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id (get_id declfrom) ++
+ user_err ~hdr:"move_hyp" (str "Cannot move " ++ pr_id (NamedDecl.get_id declfrom) ++
Miscprint.pr_move_location pr_id hto ++
str (if toleft then ": it occurs in " else ": it depends on ")
++ pr_id hyp ++ str ".")
@@ -287,7 +289,7 @@ let move_hyp toleft (left,declfrom,right) hto =
variables only in Application and Case *)
let error_unsupported_deep_meta c =
- errorlabstrm "" (strbrk "Application of lemmas whose beta-iota normal " ++
+ user_err (strbrk "Application of lemmas whose beta-iota normal " ++
strbrk "form contains metavariables deep inside the term is not " ++
strbrk "supported; try \"refine\" instead.")
@@ -295,9 +297,9 @@ let collect_meta_variables c =
let rec collrec deep acc c = match kind_of_term c with
| Meta mv -> if deep then error_unsupported_deep_meta () else mv::acc
| Cast(c,_,_) -> collrec deep acc c
- | (App _| Case _) -> fold_constr (collrec deep) acc c
+ | (App _| Case _) -> Term.fold_constr (collrec deep) acc c
| Proj (_, c) -> collrec deep acc c
- | _ -> fold_constr (collrec true) acc c
+ | _ -> Term.fold_constr (collrec true) acc c
in
List.rev (collrec false [] c)
@@ -489,19 +491,20 @@ and mk_casegoals sigma goal goalacc p c =
let convert_hyp check sign sigma d =
- let id,b,bt = to_tuple d in
+ let id = NamedDecl.get_id d in
+ let b = NamedDecl.get_value d in
let env = Global.env() in
let reorder = ref [] in
let sign' =
apply_to_hyp check sign id
(fun _ d' _ ->
- let _,c,ct = to_tuple d' in
+ let c = NamedDecl.get_value d' in
let env = Global.env_of_context sign in
- if check && not (is_conv env sigma bt ct) then
- errorlabstrm "Logic.convert_hyp"
+ if check && not (is_conv env sigma (NamedDecl.get_type d) (NamedDecl.get_type d')) then
+ user_err ~hdr:"Logic.convert_hyp"
(str "Incorrect change of the type of " ++ pr_id id ++ str ".");
if check && not (Option.equal (is_conv env sigma) b c) then
- errorlabstrm "Logic.convert_hyp"
+ user_err ~hdr:"Logic.convert_hyp"
(str "Incorrect change of the body of "++ pr_id id ++ str ".");
if check then reorder := check_decl_position env sign d;
d) in
@@ -534,7 +537,7 @@ let prim_refiner r sigma goal =
t,cl,sigma
else
(if !check && mem_named_context id (named_context_of_val sign) then
- errorlabstrm "Logic.prim_refiner"
+ user_err ~hdr:"Logic.prim_refiner"
(str "Variable " ++ pr_id id ++ str " is already declared.");
push_named_context_val (LocalAssum (id,t)) sign,t,cl,sigma) in
let (sg2,ev2,sigma) =
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index e4bae20128..86c2b7a573 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -131,7 +131,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
| CList.IndexOutOfRange ->
match gi with
| Vernacexpr.SelectNth i -> let msg = str "No such goal: " ++ int i ++ str "." in
- CErrors.errorlabstrm "" msg
+ CErrors.user_err msg
| _ -> assert false
let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac)
@@ -228,7 +228,7 @@ let solve_by_implicit_tactic env sigma evk =
when
Context.Named.equal (Environ.named_context_of_val evi.evar_hyps)
(Environ.named_context env) ->
- let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError ("",Pp.str"Proof is not complete."))) []) in
+ let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError (None,Pp.str"Proof is not complete."))) []) in
(try
let c = Evarutil.nf_evars_universes sigma evi.evar_concl in
if Evarutil.has_undefined_evars sigma c then raise Exit;
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 666730e1af..9b0200039b 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -130,8 +130,8 @@ val set_end_tac : Tacexpr.raw_tactic_expr -> unit
(** [set_used_variables l] declares that section variables [l] will be
used in the proof *)
val set_used_variables :
- Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list
-val get_used_variables : unit -> Context.section_context option
+ Id.t list -> Context.Named.t * (Loc.t * Names.Id.t) list
+val get_used_variables : unit -> Context.Named.t option
(** {6 Universe binders } *)
val get_universe_binders : unit -> universe_binders option
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 5fe29653d3..16278b456a 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -68,9 +68,9 @@ let _ = CErrors.register_handler begin function
| CannotUnfocusThisWay ->
CErrors.error "This proof is focused, but cannot be unfocused this way"
| NoSuchGoals (i,j) when Int.equal i j ->
- CErrors.errorlabstrm "Focus" Pp.(str"No such goal (" ++ int i ++ str").")
+ CErrors.user_err ~hdr:"Focus" Pp.(str"No such goal (" ++ int i ++ str").")
| NoSuchGoals (i,j) ->
- CErrors.errorlabstrm "Focus" Pp.(
+ CErrors.user_err ~hdr:"Focus" Pp.(
str"Not every goal in range ["++ int i ++ str","++int j++str"] exist."
)
| FullyUnfocused -> CErrors.error "The proof is not focused"
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 7605f63872..f3ca19a903 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -18,6 +18,8 @@ open Util
open Pp
open Names
+module NamedDecl = Context.Named.Declaration
+
(*** Proof Modes ***)
(* Type of proof modes :
@@ -89,7 +91,7 @@ type pstate = {
pid : Id.t;
terminator : proof_terminator CEphemeron.key;
endline_tactic : Tacexpr.raw_tactic_expr option;
- section_vars : Context.section_context option;
+ section_vars : Context.Named.t option;
proof : Proof.proof;
strength : Decl_kinds.goal_kind;
mode : proof_mode CEphemeron.key;
@@ -202,8 +204,8 @@ let discard (loc,id) =
let n = List.length !pstates in
discard_gen id;
if Int.equal (List.length !pstates) n then
- CErrors.user_err_loc
- (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs ())
+ CErrors.user_err ~loc
+ ~hdr:"Pfedit.delete_proof" (str"No such proof" ++ msg_proofs ())
let discard_current () =
if List.is_empty !pstates then raise NoCurrentProof else pstates := List.tl !pstates
@@ -276,7 +278,7 @@ let set_used_variables l =
let ids = List.fold_right Id.Set.add l Id.Set.empty in
let ctx = Environ.keep_hyps env ids in
let ctx_set =
- List.fold_right Id.Set.add (List.map get_id ctx) Id.Set.empty in
+ List.fold_right Id.Set.add (List.map NamedDecl.get_id ctx) Id.Set.empty in
let vars_of = Environ.global_vars_set in
let aux env entry (ctx, all_safe, to_clear as orig) =
match entry with
@@ -408,7 +410,7 @@ let return_proof ?(allow_partial=false) () =
let evd =
let error s =
let prf = str " (in proof " ++ Id.print pid ++ str ")" in
- raise (CErrors.UserError("last tactic before Qed",s ++ prf))
+ raise (CErrors.UserError(Some "last tactic before Qed",s ++ prf))
in
try Proof.return proof with
| Proof.UnfinishedProof ->
@@ -519,7 +521,7 @@ module Bullet = struct
(function
| FailedBullet (b,sugg) ->
let prefix = str"Wrong bullet " ++ pr_bullet b ++ str" : " in
- CErrors.errorlabstrm "Focus" (prefix ++ suggest_on_error sugg)
+ CErrors.user_err ~hdr:"Focus" (prefix ++ suggest_on_error sugg)
| _ -> raise CErrors.Unhandled)
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 59daa29681..86fc1deff8 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -143,8 +143,8 @@ val set_interp_tac :
* (w.r.t. type dependencies and let-ins covered by it) + a list of
* ids to be cleared *)
val set_used_variables :
- Names.Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list
-val get_used_variables : unit -> Context.section_context option
+ Names.Id.t list -> Context.Named.t * (Loc.t * Names.Id.t) list
+val get_used_variables : unit -> Context.Named.t option
val get_universe_binders : unit -> universe_binders option
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index caa9b328a0..a125fb10db 100644
--- a/proofs/proof_using.ml
+++ b/proofs/proof_using.ml
@@ -12,6 +12,8 @@ open Util
open Vernacexpr
open Context.Named.Declaration
+module NamedDecl = Context.Named.Declaration
+
let to_string e =
let rec aux = function
| SsEmpty -> "()"
@@ -35,12 +37,14 @@ let in_nameset =
let rec close_fwd e s =
let s' =
List.fold_left (fun s decl ->
- let (id,b,ty) = Context.Named.Declaration.to_tuple decl in
- let vb = Option.(default Id.Set.empty (map (global_vars_set e) b)) in
- let vty = global_vars_set e ty in
+ let vb = match decl with
+ | LocalAssum _ -> Id.Set.empty
+ | LocalDef (_,b,_) -> global_vars_set e b
+ in
+ let vty = global_vars_set e (NamedDecl.get_type decl) in
let vbty = Id.Set.union vb vty in
if Id.Set.exists (fun v -> Id.Set.mem v s) vbty
- then Id.Set.add id (Id.Set.union s vbty) else s)
+ then Id.Set.add (NamedDecl.get_id decl) (Id.Set.union s vbty) else s)
s (named_context e)
in
if Id.Set.equal s s' then s else close_fwd e s'
@@ -63,13 +67,13 @@ and set_of_id env ty id =
Id.Set.union (global_vars_set env ty) acc)
Id.Set.empty ty
else if Id.to_string id = "All" then
- List.fold_right Id.Set.add (List.map get_id (named_context env)) Id.Set.empty
+ List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty
else if CList.mem_assoc_f Id.equal id !known_names then
process_expr env (CList.assoc_f Id.equal id !known_names) []
else Id.Set.singleton id
and full_set env =
- List.fold_right Id.Set.add (List.map get_id (named_context env)) Id.Set.empty
+ List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty
let process_expr env e ty =
let ty_expr = SsSingl(Loc.ghost, Id.of_string "Type") in
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 72cb05f1b6..34443b93da 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -73,7 +73,7 @@ let set_strategy_one ref l =
let cb = Global.lookup_constant sp in
(match cb.const_body with
| OpaqueDef _ ->
- errorlabstrm "set_transparent_const"
+ user_err ~hdr:"set_transparent_const"
(str "Cannot make" ++ spc () ++
Nametab.pr_global_env Id.Set.empty (ConstRef sp) ++
spc () ++ str "transparent because it was declared opaque.");
@@ -175,19 +175,19 @@ let red_expr_tab = Summary.ref String.Map.empty ~name:"Declare Reduction"
let declare_reduction s f =
if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab
- then errorlabstrm "Redexpr.declare_reduction"
+ then user_err ~hdr:"Redexpr.declare_reduction"
(str "There is already a reduction expression of name " ++ str s)
else reduction_tab := String.Map.add s f !reduction_tab
let check_custom = function
| ExtraRedExpr s ->
if not (String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab)
- then errorlabstrm "Redexpr.check_custom" (str "Reference to undefined reduction expression " ++ str s)
+ then user_err ~hdr:"Redexpr.check_custom" (str "Reference to undefined reduction expression " ++ str s)
|_ -> ()
let decl_red_expr s e =
if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab
- then errorlabstrm "Redexpr.decl_red_expr"
+ then user_err ~hdr:"Redexpr.decl_red_expr"
(str "There is already a reduction expression of name " ++ str s)
else begin
check_custom e;
@@ -247,7 +247,7 @@ let reduction_of_red_expr env =
with Not_found ->
(try reduction_of_red_expr (String.Map.find s !red_expr_tab)
with Not_found ->
- errorlabstrm "Redexpr.reduction_of_red_expr"
+ user_err ~hdr:"Redexpr.reduction_of_red_expr"
(str "unknown user-defined reduction \"" ++ str s ++ str "\"")))
| CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast)
| CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast)
diff --git a/proofs/refine.ml b/proofs/refine.ml
index af9be78974..28952b9a75 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -11,6 +11,8 @@ open Sigma.Notations
open Proofview.Notations
open Context.Named.Declaration
+module NamedDecl = Context.Named.Declaration
+
let extract_prefix env info =
let ctx1 = List.rev (Environ.named_context env) in
let ctx2 = List.rev (Evd.evar_context info) in
@@ -26,7 +28,7 @@ let typecheck_evar ev env sigma =
let info = Evd.find sigma ev in
(** Typecheck the hypotheses. *)
let type_hyp (sigma, env) decl =
- let t = get_type decl in
+ let t = NamedDecl.get_type decl in
let evdref = ref sigma in
let _ = Typing.e_sort_of env evdref t in
let () = match decl with
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index ea8543b02f..9a0b56b84b 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -13,7 +13,8 @@ open Evd
open Environ
open Proof_type
open Logic
-open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
let sig_it x = x.it
let project x = x.sigma
@@ -60,7 +61,7 @@ let tclIDTAC_MESSAGE s gls =
Feedback.msg_info (hov 0 s); tclIDTAC gls
(* General failure tactic *)
-let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s)
+let tclFAIL_s s gls = user_err ~hdr:"Refiner.tclFAIL_s" (str s)
(* A special exception for levels for the Fail tactic *)
exception FailError of int * std_ppcmds Lazy.t
@@ -82,7 +83,7 @@ let thens3parts_tac tacfi tac tacli (sigr,gs) =
let nf = Array.length tacfi in
let nl = Array.length tacli in
let ng = List.length gs in
- if ng<nf+nl then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals.");
+ if ng<nf+nl then user_err ~hdr:"Refiner.thensn_tac" (str "Not enough subgoals.");
let gll =
(List.map_i (fun i ->
apply_sig_tac sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac))
@@ -164,14 +165,14 @@ the goal unchanged *)
let tclWEAK_PROGRESS tac ptree =
let rslt = tac ptree in
if Goal.V82.weak_progress rslt ptree then rslt
- else errorlabstrm "Refiner.WEAK_PROGRESS" (str"Failed to progress.")
+ else user_err ~hdr:"Refiner.WEAK_PROGRESS" (str"Failed to progress.")
(* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves
the goal unchanged *)
let tclPROGRESS tac ptree =
let rslt = tac ptree in
if Goal.V82.progress rslt ptree then rslt
- else errorlabstrm "Refiner.PROGRESS" (str"Failed to progress.")
+ else user_err ~hdr:"Refiner.PROGRESS" (str"Failed to progress.")
(* Same as tclWEAK_PROGRESS but fails also if tactics generates several goals,
one of them being identical to the original goal *)
@@ -182,7 +183,7 @@ let tclNOTSAMEGOAL (tac : tactic) goal =
let rslt = tac goal in
let {it=gls;sigma=sigma} = rslt in
if List.exists (same_goal goal sigma) gls
- then errorlabstrm "Refiner.tclNOTSAMEGOAL"
+ then user_err ~hdr:"Refiner.tclNOTSAMEGOAL"
(str"Tactic generated a subgoal identical to the original goal.")
else rslt
@@ -202,7 +203,7 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
let { it = gls; sigma = sigma; } = rslt in
let hyps:Context.Named.t list =
List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in
- let cmp d1 d2 = Names.Id.equal (get_id d1) (get_id d2) in
+ let cmp d1 d2 = Names.Id.equal (NamedDecl.get_id d1) (NamedDecl.get_id d2) in
let newhyps =
List.map
(fun hypl -> List.subtract cmp hypl oldhyps)
@@ -215,7 +216,7 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
List.fold_left
(fun acc lh -> acc ^ (if !frst then (frst:=false;"") else " | ")
^ (List.fold_left
- (fun acc d -> (Names.Id.to_string (get_id d)) ^ " " ^ acc)
+ (fun acc d -> (Names.Id.to_string (NamedDecl.get_id d)) ^ " " ^ acc)
"" lh))
"" newhyps in
Feedback.msg_notice
@@ -316,7 +317,7 @@ let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl)
let tclDO n t =
let rec dorec k =
- if k < 0 then errorlabstrm "Refiner.tclDO"
+ if k < 0 then user_err ~hdr:"Refiner.tclDO"
(str"Wrong argument : Do needs a positive integer.");
if Int.equal k 0 then tclIDTAC
else if Int.equal k 1 then t else (tclTHEN t (dorec (k-1)))
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 50984c48e0..93e276f4ba 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -21,6 +21,8 @@ open Refiner
open Sigma.Notations
open Context.Named.Declaration
+module NamedDecl = Context.Named.Declaration
+
let re_sig it gc = { it = it; sigma = gc; }
(**************************************************************)
@@ -46,7 +48,7 @@ let pf_hyps_types gls =
| LocalDef (id,_,x) -> id, x)
sign
-let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> get_id
+let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> NamedDecl.get_id
let pf_last_hyp gl = List.hd (pf_hyps gl)
@@ -57,7 +59,7 @@ let pf_get_hyp gls id =
raise (RefinerError (NoSuchHyp id))
let pf_get_hyp_typ gls id =
- pf_get_hyp gls id |> get_type
+ id |> pf_get_hyp gls |> NamedDecl.get_type
let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls)
@@ -101,7 +103,7 @@ let pf_const_value = pf_reduce (fun env _ -> constant_value_in env)
let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind
let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind
-let pf_hnf_type_of gls = pf_whd_all gls % pf_get_type_of gls
+let pf_hnf_type_of gls = pf_get_type_of gls %> pf_whd_all gls
let pf_is_matching = pf_apply Constr_matching.is_matching_conv
let pf_matches = pf_apply Constr_matching.matches_conv
@@ -199,7 +201,7 @@ module New = struct
sign
let pf_get_hyp_typ id gl =
- pf_get_hyp id gl |> get_type
+ pf_get_hyp id gl |> NamedDecl.get_type
let pf_hyps_types gl =
let env = Proofview.Goal.env gl in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 01:02:10 +0000