aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.ml17
-rw-r--r--proofs/clenvtac.mli1
-rw-r--r--proofs/evar_refiner.ml6
-rw-r--r--proofs/goal.ml3
-rw-r--r--proofs/goal.mli3
-rw-r--r--proofs/logic.ml9
-rw-r--r--proofs/pfedit.ml12
-rw-r--r--proofs/pfedit.mli4
-rw-r--r--proofs/proof.ml16
-rw-r--r--proofs/proof_global.ml72
-rw-r--r--proofs/proof_global.mli5
-rw-r--r--proofs/proof_type.mli3
-rw-r--r--proofs/proof_using.ml8
-rw-r--r--proofs/redexpr.ml4
-rw-r--r--proofs/refine.ml23
-rw-r--r--proofs/refine.mli6
-rw-r--r--proofs/refiner.ml21
-rw-r--r--proofs/refiner.mli2
-rw-r--r--proofs/tacmach.ml3
-rw-r--r--proofs/tacmach.mli1
20 files changed, 95 insertions, 124 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index f9ebc42330..33a86402ef 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -27,11 +27,6 @@ open Unification
open Misctypes
open Sigma.Notations
-(* Abbreviations *)
-
-let pf_env = Refiner.pf_env
-let pf_type_of gls c = Typing.unsafe_type_of (pf_env gls) gls.sigma c
-
(******************************************************************)
(* Clausal environments *)
@@ -168,7 +163,7 @@ let error_incompatible_inst clenv mv =
let clenv_assign mv rhs clenv =
let rhs_fls = mk_freelisted rhs in
if Metaset.exists (mentions clenv mv) rhs_fls.freemetas then
- error "clenv_assign: circularity in unification";
+ user_err Pp.(str "clenv_assign: circularity in unification");
try
if meta_defined clenv.evd mv then
if not (EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd mv)).rebus) rhs) then
@@ -179,7 +174,7 @@ let clenv_assign mv rhs clenv =
let st = (Conv,TypeNotProcessed) in
{clenv with evd = meta_assign mv (EConstr.Unsafe.to_constr rhs_fls.rebus,st) clenv.evd}
with Not_found ->
- error "clenv_assign: undefined meta"
+ user_err Pp.(str "clenv_assign: undefined meta")
@@ -421,7 +416,7 @@ let qhyp_eq h1 h2 = match h1, h2 with
| _ -> false
let check_bindings bl =
- match List.duplicates qhyp_eq (List.map pi2 bl) with
+ match List.duplicates qhyp_eq (List.map (fun x -> fst (snd x)) bl) with
| NamedHyp s :: _ ->
user_err
(str "The variable " ++ pr_id s ++
@@ -517,7 +512,7 @@ let clenv_match_args bl clenv =
let mvs = clenv_independent clenv in
check_bindings bl;
List.fold_left
- (fun clenv (loc,b,c) ->
+ (fun clenv (loc,(b,c)) ->
let k = meta_of_binder clenv loc mvs b in
if meta_defined clenv.evd k then
if EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd k)).rebus) c then clenv
@@ -681,7 +676,7 @@ let define_with_type sigma env ev c =
let t = Retyping.get_type_of env sigma ev in
let ty = Retyping.get_type_of env sigma c in
let j = Environ.make_judge c ty in
- let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j t in
+ let (sigma, j) = Coercion.inh_conv_coerce_to true env sigma j t in
let (ev, _) = destEvar sigma ev in
let sigma = Evd.define ev (EConstr.Unsafe.to_constr j.Environ.uj_val) sigma in
sigma
@@ -716,7 +711,7 @@ let solve_evar_clause env sigma hyp_only clause = function
error_not_right_number_missing_arguments len
| ExplicitBindings lbind ->
let () = check_bindings lbind in
- let fold sigma (_, binder, c) =
+ let fold sigma (_, (binder, c)) =
let ev = evar_of_binder clause.cl_holes binder in
define_with_type sigma env ev c
in
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 5b7164705a..26069207eb 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -8,7 +8,6 @@
(** Legacy components of the previous proof engine. *)
-open Term
open Clenv
open EConstr
open Unification
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 8367c09b8f..b1fe128a24 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -39,11 +39,11 @@ let define_and_solve_constraints evk c env evd =
pbs
with
| Success evd -> evd
- | UnifFailure _ -> error "Instance does not satisfy the constraints."
+ | UnifFailure _ -> user_err Pp.(str "Instance does not satisfy the constraints.")
let w_refine (evk,evi) (ltac_var,rawc) sigma =
if Evd.is_defined sigma evk then
- error "Instantiate called on already-defined evar";
+ user_err Pp.(str "Instantiate called on already-defined evar");
let env = Evd.evar_filtered_env evi in
let sigma',typed_c =
let flags = {
@@ -56,7 +56,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
env sigma ltac_var (Pretyping.OfType (EConstr.of_constr evi.evar_concl)) rawc
with e when CErrors.noncritical e ->
let loc = Glob_ops.loc_of_glob_constr rawc in
- user_err ~loc
+ user_err ?loc
(str "Instance is not well-typed in the environment of " ++
Termops.pr_existential_key sigma evk ++ str ".")
in
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 9046f45341..5a717f1662 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -8,7 +8,6 @@
open Util
open Pp
-open Term
open Sigma.Notations
module NamedDecl = Context.Named.Declaration
@@ -69,7 +68,7 @@ module V82 = struct
Evd.evar_concl = concl;
Evd.evar_filter = Evd.Filter.identity;
Evd.evar_body = Evd.Evar_empty;
- Evd.evar_source = (Loc.ghost,Evar_kinds.GoalEvar);
+ Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar);
Evd.evar_candidates = None;
Evd.evar_extra = extra }
in
diff --git a/proofs/goal.mli b/proofs/goal.mli
index a2fa34c05e..ee2e736120 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -59,9 +59,6 @@ module V82 : sig
second goal *)
val partial_solution_to : Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map
- (* Principal part of the weak-progress tactical *)
- val weak_progress : goal list Evd.sigma -> goal Evd.sigma -> bool
-
(* Principal part of the progress tactical *)
val progress : goal list Evd.sigma -> goal Evd.sigma -> bool
diff --git a/proofs/logic.ml b/proofs/logic.ml
index e6024785db..cd2cfbd32f 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -97,11 +97,6 @@ let check_typability env sigma c =
(instead of iterating on the list of identifier to be removed, which
forces the user to give them in order). *)
-let clear_hyps env sigma ids sign cl =
- let evdref = ref (Evd.clear_metas sigma) in
- let (hyps,cl) = Evarutil.clear_hyps_in_evi env evdref sign cl ids in
- (hyps, cl, !evdref)
-
let clear_hyps2 env sigma ids sign t cl =
let evdref = ref (Evd.clear_metas sigma) in
let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in
@@ -146,7 +141,7 @@ let occur_vars_in_decl env sigma hyps d =
let reorder_context env sigma sign ord =
let ords = List.fold_right Id.Set.add ord Id.Set.empty in
if not (Int.equal (List.length ord) (Id.Set.cardinal ords)) then
- error "Order list has duplicates";
+ user_err Pp.(str "Order list has duplicates");
let rec step ord expected ctxt_head moved_hyps ctxt_tail =
match ord with
| [] -> List.rev ctxt_tail @ ctxt_head
@@ -379,7 +374,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
let (acc',hdty,sigma,applicand) =
if is_template_polymorphic env sigma (EConstr.of_constr f) then
let ty =
- (* Template sort-polymorphism of definition and inductive types *)
+ (* Template polymorphism of definitions and inductive types *)
let firstmeta = Array.findi (fun i x -> occur_meta sigma (EConstr.of_constr x)) l in
let args, _ = Option.cata (fun i -> CArray.chop i l) (l, [||]) firstmeta in
type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) (Array.map EConstr.of_constr args)
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 7e8ed31d1d..aaceb7b762 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -15,7 +15,7 @@ open Evd
let use_unification_heuristics_ref = ref true
let _ = Goptions.declare_bool_option {
- Goptions.optsync = true; Goptions.optdepr = false;
+ Goptions.optdepr = false;
Goptions.optname = "Solve unification constraints at every \".\"";
Goptions.optkey = ["Solve";"Unification";"Constraints"];
Goptions.optread = (fun () -> !use_unification_heuristics_ref);
@@ -71,7 +71,7 @@ let get_universe_binders () =
exception NoSuchGoal
let _ = CErrors.register_handler begin function
- | NoSuchGoal -> CErrors.error "No such goal."
+ | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.")
| _ -> raise CErrors.Unhandled
end
let get_nth_V82_goal i =
@@ -87,12 +87,12 @@ let get_goal_context_gen i =
let get_goal_context i =
try get_goal_context_gen i
- with Proof_global.NoCurrentProof -> CErrors.error "No focused proof."
- | NoSuchGoal -> CErrors.error "No such goal."
+ with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof.")
+ | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.")
let get_current_goal_context () =
try get_goal_context_gen 1
- with Proof_global.NoCurrentProof -> CErrors.error "No focused proof."
+ with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof.")
| NoSuchGoal ->
(* spiwack: returning empty evar_map, since if there is no goal, under focus,
there is no accessible evar either *)
@@ -143,7 +143,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
in
(p,status)
with
- Proof_global.NoCurrentProof -> CErrors.error "No focused proof"
+ Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof")
let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index f9fb0b76de..1bf65b8aed 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -130,7 +130,7 @@ val set_end_tac : Genarg.glob_generic_argument -> unit
(** [set_used_variables l] declares that section variables [l] will be
used in the proof *)
val set_used_variables :
- Id.t list -> Context.Named.t * (Loc.t * Names.Id.t) list
+ Id.t list -> Context.Named.t * Names.Id.t Loc.located list
val get_used_variables : unit -> Context.Named.t option
(** {6 Universe binders } *)
@@ -190,4 +190,4 @@ val declare_implicit_tactic : unit Proofview.tactic -> unit
val clear_implicit_tactic : unit -> unit
(* Raise Exit if cannot solve *)
-val solve_by_implicit_tactic : unit -> (env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * EConstr.constr) option
+val solve_by_implicit_tactic : unit -> Pretyping.inference_hook option
diff --git a/proofs/proof.ml b/proofs/proof.ml
index b2103489a7..2aa620c1da 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -66,14 +66,14 @@ exception FullyUnfocused
let _ = CErrors.register_handler begin function
| CannotUnfocusThisWay ->
- CErrors.error "This proof is focused, but cannot be unfocused this way"
+ CErrors.user_err Pp.(str "This proof is focused, but cannot be unfocused this way")
| NoSuchGoals (i,j) when Int.equal i j ->
CErrors.user_err ~hdr:"Focus" Pp.(str"No such goal (" ++ int i ++ str").")
| NoSuchGoals (i,j) ->
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"
+ | FullyUnfocused -> CErrors.user_err Pp.(str "The proof is not focused")
| _ -> raise CErrors.Unhandled
end
@@ -301,10 +301,10 @@ exception HasShelvedGoals
exception HasGivenUpGoals
exception HasUnresolvedEvar
let _ = CErrors.register_handler begin function
- | UnfinishedProof -> CErrors.error "Some goals have not been solved."
- | HasShelvedGoals -> CErrors.error "Some goals have been left on the shelf."
- | HasGivenUpGoals -> CErrors.error "Some goals have been given up."
- | HasUnresolvedEvar -> CErrors.error "Some existential variables are uninstantiated."
+ | UnfinishedProof -> CErrors.user_err Pp.(str "Some goals have not been solved.")
+ | HasShelvedGoals -> CErrors.user_err Pp.(str "Some goals have been left on the shelf.")
+ | HasGivenUpGoals -> CErrors.user_err Pp.(str "Some goals have been given up.")
+ | HasUnresolvedEvar -> CErrors.user_err Pp.(str "Some existential variables are uninstantiated.")
| _ -> raise CErrors.Unhandled
end
@@ -420,9 +420,9 @@ module V82 = struct
let evl = Evarutil.non_instantiated sigma in
let evl = Evar.Map.bindings evl in
if (n <= 0) then
- CErrors.error "incorrect existential variable index"
+ CErrors.user_err Pp.(str "incorrect existential variable index")
else if CList.length evl < n then
- CErrors.error "not so many uninstantiated existential variables"
+ CErrors.user_err Pp.(str "not so many uninstantiated existential variables")
else
CList.nth evl (n-1)
in
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index e4cba6f07d..4d2f534a76 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -36,7 +36,7 @@ let proof_modes = Hashtbl.create 6
let find_proof_mode n =
try Hashtbl.find proof_modes n
with Not_found ->
- CErrors.error (Format.sprintf "No proof mode named \"%s\"." n)
+ CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." n))
let register_proof_mode ({name = n} as m) =
Hashtbl.add proof_modes n (CEphemeron.create m)
@@ -52,8 +52,7 @@ let get_default_proof_mode_name () =
(CEphemeron.default !default_proof_mode standard).name
let _ =
- Goptions.declare_string_option {Goptions.
- optsync = true ;
+ Goptions.(declare_string_option {
optdepr = false;
optname = "default proof mode" ;
optkey = ["Default";"Proof";"Mode"] ;
@@ -63,7 +62,7 @@ let _ =
optwrite = begin fun n ->
default_proof_mode := find_proof_mode n
end
- }
+ })
(*** Proof Global Environment ***)
@@ -82,13 +81,13 @@ type proof_object = {
type proof_ending =
| Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes
| Proved of Vernacexpr.opacity_flag *
- (Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
+ Vernacexpr.lident option *
proof_object
type proof_terminator = proof_ending -> unit
type closed_proof = proof_object * proof_terminator
type pstate = {
- pid : Id.t;
+ pid : Id.t; (* the name of the theorem whose proof is being constructed *)
terminator : proof_terminator CEphemeron.key;
endline_tactic : Genarg.glob_generic_argument option;
section_vars : Context.Named.t option;
@@ -125,13 +124,13 @@ let push a l = l := a::!l;
exception NoSuchProof
let _ = CErrors.register_handler begin function
- | NoSuchProof -> CErrors.error "No such proof."
+ | NoSuchProof -> CErrors.user_err Pp.(str "No such proof.")
| _ -> raise CErrors.Unhandled
end
exception NoCurrentProof
let _ = CErrors.register_handler begin function
- | NoCurrentProof -> CErrors.error "No focused proof (No proof-editing in progress)."
+ | NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).")
| _ -> raise CErrors.Unhandled
end
@@ -207,7 +206,7 @@ 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
+ CErrors.user_err ?loc
~hdr:"Pfedit.delete_proof" (str"No such proof" ++ msg_proofs ())
let discard_current () =
@@ -268,8 +267,7 @@ let get_universe_binders () = (cur_pstate ()).universe_binders
let proof_using_auto_clear = ref false
let _ = Goptions.declare_bool_option
- { Goptions.optsync = true;
- Goptions.optdepr = false;
+ { Goptions.optdepr = false;
Goptions.optname = "Proof using Clear Unused";
Goptions.optkey = ["Proof";"Using";"Clear";"Unused"];
Goptions.optread = (fun () -> !proof_using_auto_clear);
@@ -287,13 +285,13 @@ let set_used_variables l =
match entry with
| LocalAssum (x,_) ->
if Id.Set.mem x all_safe then orig
- else (ctx, all_safe, (Loc.ghost,x)::to_clear)
+ else (ctx, all_safe, (Loc.tag x)::to_clear)
| LocalDef (x,bo, ty) as decl ->
if Id.Set.mem x all_safe then orig else
let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in
if Id.Set.subset vars all_safe
then (decl :: ctx, Id.Set.add x all_safe, to_clear)
- else (ctx, all_safe, (Loc.ghost,x) :: to_clear) in
+ else (ctx, all_safe, (Loc.tag x) :: to_clear) in
let ctx, _, to_clear =
Environ.fold_named_context aux env ~init:(ctx,ctx_set,[]) in
let to_clear = if !proof_using_auto_clear then to_clear else [] in
@@ -301,7 +299,7 @@ let set_used_variables l =
| [] -> raise NoCurrentProof
| p :: rest ->
if not (Option.is_empty p.section_vars) then
- CErrors.error "Used section variables can be declared only once";
+ CErrors.user_err Pp.(str "Used section variables can be declared only once");
pstates := { p with section_vars = Some ctx} :: rest;
ctx, to_clear
@@ -516,7 +514,7 @@ module Bullet = struct
| NeedClosingBrace -> str"Try unfocusing with \"}\"."
| NoBulletInUse -> assert false (* This should never raise an error. *)
| ProofFinished -> str"No more subgoals."
- | Suggest b -> str"Bullet " ++ pr_bullet b ++ str" is mandatory here."
+ | Suggest b -> str"Expecting " ++ pr_bullet b ++ str"."
| Unfinished b -> str"Current bullet " ++ pr_bullet b ++ str" is not finished."
exception FailedBullet of t * suggestion
@@ -525,7 +523,7 @@ module Bullet = struct
CErrors.register_handler
(function
| FailedBullet (b,sugg) ->
- let prefix = str"Wrong bullet " ++ pr_bullet b ++ str" : " in
+ let prefix = str"Wrong bullet " ++ pr_bullet b ++ str": " in
CErrors.user_err ~hdr:"Focus" (prefix ++ suggest_on_error sugg)
| _ -> raise CErrors.Unhandled)
@@ -628,8 +626,7 @@ module Bullet = struct
let current_behavior = ref Strict.strict
let _ =
- Goptions.declare_string_option {Goptions.
- optsync = true;
+ Goptions.(declare_string_option {
optdepr = false;
optname = "bullet behavior";
optkey = ["Bullet";"Behavior"];
@@ -640,9 +637,9 @@ module Bullet = struct
current_behavior :=
try Hashtbl.find behaviors n
with Not_found ->
- CErrors.error ("Unknown bullet behavior: \"" ^ n ^ "\".")
+ CErrors.user_err Pp.(str ("Unknown bullet behavior: \"" ^ n ^ "\"."))
end
- }
+ })
let put p b =
(!current_behavior).put p b
@@ -671,16 +668,18 @@ let _ =
let default_goal_selector = ref (Vernacexpr.SelectNth 1)
let get_default_goal_selector () = !default_goal_selector
-let print_range_selector (i, j) =
- if i = j then string_of_int i
- else string_of_int i ^ "-" ^ string_of_int j
+let pr_range_selector (i, j) =
+ if i = j then int i
+ else int i ++ str "-" ++ int j
-let print_goal_selector = function
- | Vernacexpr.SelectAll -> "all"
- | Vernacexpr.SelectNth i -> string_of_int i
- | Vernacexpr.SelectList l -> "[" ^
- String.concat ", " (List.map print_range_selector l) ^ "]"
- | Vernacexpr.SelectId id -> Id.to_string id
+let pr_goal_selector = function
+ | Vernacexpr.SelectAll -> str "all"
+ | Vernacexpr.SelectNth i -> int i
+ | Vernacexpr.SelectList l ->
+ str "["
+ ++ prlist_with_sep pr_comma pr_range_selector l
+ ++ str "]"
+ | Vernacexpr.SelectId id -> Id.print id
let parse_goal_selector = function
| "all" -> Vernacexpr.SelectAll
@@ -688,22 +687,23 @@ let parse_goal_selector = function
let err_msg = "The default selector must be \"all\" or a natural number." in
begin try
let i = int_of_string i in
- if i < 0 then CErrors.error err_msg;
+ if i < 0 then CErrors.user_err Pp.(str err_msg);
Vernacexpr.SelectNth i
- with Failure _ -> CErrors.error err_msg
+ with Failure _ -> CErrors.user_err Pp.(str err_msg)
end
let _ =
- Goptions.declare_string_option {Goptions.
- optsync = true ;
- optdepr = false;
+ Goptions.(declare_string_option{optdepr = false;
optname = "default goal selector" ;
optkey = ["Default";"Goal";"Selector"] ;
- optread = begin fun () -> print_goal_selector !default_goal_selector end;
+ optread = begin fun () ->
+ string_of_ppcmds
+ (pr_goal_selector !default_goal_selector)
+ end;
optwrite = begin fun n ->
default_goal_selector := parse_goal_selector n
end
- }
+ })
module V82 = struct
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 3b2cc6b23b..52bbd9ac56 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -70,7 +70,7 @@ type proof_ending =
| Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
proof_universes
| Proved of Vernacexpr.opacity_flag *
- (Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
+ Vernacexpr.lident option *
proof_object
type proof_terminator
type closed_proof = proof_object * proof_terminator
@@ -140,7 +140,7 @@ val set_endline_tactic : Genarg.glob_generic_argument -> unit
* (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.Named.t * (Loc.t * Names.Id.t) list
+ Names.Id.t list -> Context.Named.t * Names.Id.t Loc.located list
val get_used_variables : unit -> Context.Named.t option
val get_universe_binders : unit -> universe_binders option
@@ -198,6 +198,7 @@ end
(* *)
(**********************************************************)
+val pr_goal_selector : Vernacexpr.goal_selector -> Pp.std_ppcmds
val get_default_goal_selector : unit -> Vernacexpr.goal_selector
module V82 : sig
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 03bc5e4710..e59db9e427 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -11,9 +11,6 @@
open Evd
open Names
open Term
-open Glob_term
-open Nametab
-open Misctypes
(** This module defines the structure of proof tree and the tactic type. So, it
is used by [Proof_tree] and [Refiner] *)
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index 2c489d6ded..f701f7cfed 100644
--- a/proofs/proof_using.ml
+++ b/proofs/proof_using.ml
@@ -76,7 +76,7 @@ and full_set env =
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
+ let ty_expr = SsSingl(Loc.tag @@ Id.of_string "Type") in
let v_ty = process_expr env ty_expr ty in
let s = Id.Set.union v_ty (process_expr env e ty) in
Id.Set.elements s
@@ -144,8 +144,7 @@ let value = ref false
let _ =
Goptions.declare_bool_option
- { Goptions.optsync = true;
- Goptions.optdepr = false;
+ { Goptions.optdepr = false;
Goptions.optname = "suggest Proof using";
Goptions.optkey = ["Suggest";"Proof";"Using"];
Goptions.optread = (fun () -> !value);
@@ -159,8 +158,7 @@ let value = ref None
let _ =
Goptions.declare_stringopt_option
- { Goptions.optsync = true;
- Goptions.optdepr = false;
+ { Goptions.optdepr = false;
Goptions.optname = "default value for Proof using";
Goptions.optkey = ["Default";"Proof";"Using"];
Goptions.optread = (fun () -> !value);
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 0fe5c73f15..7cd526843a 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -43,7 +43,7 @@ let cbv_native env sigma c =
let whd_cbn flags env sigma t =
let (state,_) =
- (whd_state_gen true true flags env sigma (t,Reductionops.Stack.empty))
+ (whd_state_gen ~refold:true ~tactic_mode:true flags env sigma (t,Reductionops.Stack.empty))
in
Reductionops.Stack.zip ~refold:true sigma state
@@ -52,7 +52,7 @@ let strong_cbn flags =
let simplIsCbn = ref (false)
let _ = Goptions.declare_bool_option {
- Goptions.optsync = true; Goptions.optdepr = false;
+ Goptions.optdepr = false;
Goptions.optname =
"Plug the simpl tactic to the new cbn mechanism";
Goptions.optkey = ["SimplIsCbn"];
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 1ee6e0ca5f..63ae41075c 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -70,8 +70,7 @@ let add_side_effect env = function
let add_side_effects env effects =
List.fold_left (fun env eff -> add_side_effect env eff) env effects
-let make_refine_enter ?(unsafe = true) f =
- { enter = fun gl ->
+let generic_refine ?(unsafe = true) f gl =
let gl = Proofview.Goal.assume gl in
let sigma = Proofview.Goal.sigma gl in
let sigma = Sigma.to_evar_map sigma in
@@ -82,7 +81,10 @@ let make_refine_enter ?(unsafe = true) f =
let prev_future_goals = Evd.future_goals sigma in
let prev_principal_goal = Evd.principal_future_goal sigma in
(** Create the refinement term *)
- let ((v,c), sigma) = Sigma.run (Evd.reset_future_goals sigma) f in
+ Proofview.Unsafe.tclEVARS (Evd.reset_future_goals sigma) >>= fun () ->
+ f >>= fun (v, c) ->
+ Proofview.tclEVARMAP >>= fun sigma ->
+ Proofview.V82.wrap_exceptions begin fun () ->
let evs = Evd.future_goals sigma in
let evkmain = Evd.principal_future_goal sigma in
(** Redo the effects in sigma in the monad's env *)
@@ -122,7 +124,18 @@ let make_refine_enter ?(unsafe = true) f =
Proofview.Unsafe.tclEVARS sigma <*>
Proofview.Unsafe.tclSETGOALS comb <*>
Proofview.tclUNIT v
- }
+ end
+
+let lift c =
+ Proofview.tclEVARMAP >>= fun sigma ->
+ Proofview.V82.wrap_exceptions begin fun () ->
+ let Sigma (c, sigma, _) = c.run (Sigma.Unsafe.of_evar_map sigma) in
+ Proofview.Unsafe.tclEVARS (Sigma.to_evar_map sigma) >>= fun () ->
+ Proofview.tclUNIT c
+ end
+
+let make_refine_enter ?unsafe f =
+ { enter = fun gl -> generic_refine ?unsafe (lift f) gl }
let refine_one ?(unsafe = true) f =
Proofview.Goal.enter_one (make_refine_enter ~unsafe f)
@@ -137,7 +150,7 @@ let with_type env evd c t =
let my_type = Retyping.get_type_of env evd c in
let j = Environ.make_judge c my_type in
let (evd,j') =
- Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t
+ Coercion.inh_conv_coerce_to true env evd j t
in
evd , j'.Environ.uj_val
diff --git a/proofs/refine.mli b/proofs/refine.mli
index 1a254d578c..5098f246a0 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -31,7 +31,11 @@ val refine : ?unsafe:bool -> EConstr.t Sigma.run -> unit tactic
type-checked beforehand. *)
val refine_one : ?unsafe:bool -> ('a * EConstr.t) Sigma.run -> 'a tactic
-(** A generalization of [refine] which assumes exactly one goal under focus *)
+(** A variant of [refine] which assumes exactly one goal under focus *)
+
+val generic_refine : ?unsafe:bool -> ('a * EConstr.t) tactic ->
+ ([ `NF ], 'r) Proofview.Goal.t -> 'a tactic
+(** The general version of refine. *)
(** {7 Helper functions} *)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 5c7659ac0e..259e96a276 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -10,7 +10,6 @@ open Pp
open CErrors
open Util
open Evd
-open Environ
open Proof_type
open Logic
@@ -162,31 +161,11 @@ let tclMAP tacfun l =
(* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves
the goal unchanged *)
-let tclWEAK_PROGRESS tac ptree =
- let rslt = tac ptree in
- if Goal.V82.weak_progress rslt ptree then rslt
- 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 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 *)
-let tclNOTSAMEGOAL (tac : tactic) goal =
- let same_goal gls1 evd2 gl2 =
- Goal.V82.same_goal gls1.sigma gls1.it evd2 gl2
- in
- let rslt = tac goal in
- let {it=gls;sigma=sigma} = rslt in
- if List.exists (same_goal goal sigma) gls
- then user_err ~hdr:"Refiner.tclNOTSAMEGOAL"
- (str"Tactic generated a subgoal identical to the original goal.")
- else rslt
-
(* Execute tac, show the names of new hypothesis names created by tac
in the "as" format and then forget everything. From the logical
point of view [tclSHOWHYPS tac] is therefore equivalent to idtac,
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 56f5facf89..e179589df2 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -119,10 +119,8 @@ val tclAT_LEAST_ONCE : tactic -> tactic
val tclFAIL : int -> Pp.std_ppcmds -> tactic
val tclFAIL_lazy : int -> Pp.std_ppcmds Lazy.t -> tactic
val tclDO : int -> tactic -> tactic
-val tclWEAK_PROGRESS : tactic -> tactic
val tclPROGRESS : tactic -> tactic
val tclSHOWHYPS : tactic -> tactic
-val tclNOTSAMEGOAL : tactic -> tactic
(** [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then,
if it succeeds, applies [tac2] to the resulting subgoals,
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index b55f8ef113..97c5cda770 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -179,9 +179,6 @@ module New = struct
let pf_unsafe_type_of gl t =
pf_apply unsafe_type_of gl t
- let pf_get_type_of gl t =
- pf_apply (Retyping.get_type_of ~lax:true) gl t
-
let pf_type_of gl t =
pf_apply type_of gl t
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 627a8e0e7e..e6e60e27f7 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -15,7 +15,6 @@ open Proof_type
open Redexpr
open Pattern
open Locus
-open Misctypes
(** Operations for handling terms under a local typing context. *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 09:49:46 +0000