aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.ml2
-rw-r--r--proofs/evar_refiner.ml4
-rw-r--r--proofs/goal_select.ml2
-rw-r--r--proofs/pfedit.ml5
-rw-r--r--proofs/pfedit.mli5
-rw-r--r--proofs/proof.ml30
-rw-r--r--proofs/proof.mli5
-rw-r--r--proofs/proof_global.ml119
-rw-r--r--proofs/proof_global.mli53
-rw-r--r--proofs/refine.ml20
-rw-r--r--proofs/refine.mli11
11 files changed, 38 insertions, 218 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 1f1bdf4da7..9540d3de44 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -677,7 +677,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 env sigma j t in
+ let (sigma, j) = Coercion.inh_conv_coerce_to ~program_mode:false true env sigma j t in
let (ev, _) = destEvar sigma ev in
let sigma = Evd.define ev j.Environ.uj_val sigma in
sigma
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 6c4193c66b..1b2756f49f 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -53,7 +53,9 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
Pretyping.use_typeclasses = true;
Pretyping.solve_unification_constraints = true;
Pretyping.fail_evar = false;
- Pretyping.expand_evars = true } in
+ Pretyping.expand_evars = true;
+ Pretyping.program_mode = false;
+ } in
try Pretyping.understand_ltac flags
env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc
with e when CErrors.noncritical e ->
diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml
index cef3fd3f5e..955d797227 100644
--- a/proofs/goal_select.ml
+++ b/proofs/goal_select.ml
@@ -45,7 +45,7 @@ let parse_goal_selector = function
| "!" -> SelectAlreadyFocused
| "all" -> SelectAll
| i ->
- let err_msg = "The default selector must be \"all\" or a natural number." in
+ 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.user_err Pp.(str err_msg);
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 7f1ae6d12b..9509c36ec0 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -70,11 +70,6 @@ let get_current_context ?p () =
let evd = Proof.in_proof p (fun x -> x) in
(evd, Global.env ())
-let current_proof_statement () =
- match Proof_global.V82.get_current_initial_conclusions () with
- | (id,([concl],strength)) -> id,strength,concl
- | _ -> CErrors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement.")
-
let solve ?with_end_tac gi info_lvl tac pr =
try
let tac = match with_end_tac with
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 5699320af5..29ab00876a 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -34,11 +34,6 @@ val get_current_goal_context : unit -> Evd.evar_map * env
val get_current_context : ?p:Proof.t -> unit -> Evd.evar_map * env
-(** [current_proof_statement] *)
-
-val current_proof_statement :
- unit -> Id.t * goal_kind * EConstr.types
-
(** {6 ... } *)
(** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 1aeb24606b..e40940f652 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -351,19 +351,13 @@ let dependent_start ~name ~poly goals =
type open_error_reason =
| UnfinishedProof
- | HasShelvedGoals
| HasGivenUpGoals
- | HasUnresolvedEvar
let print_open_error_reason er = let open Pp in match er with
| UnfinishedProof ->
str "Attempt to save an incomplete proof"
- | HasShelvedGoals ->
- str "Attempt to save a proof with shelved goals"
| HasGivenUpGoals ->
strbrk "Attempt to save a proof with given up goals. If this is really what you want to do, use Admitted in place of Qed."
- | HasUnresolvedEvar ->
- strbrk "Attempt to save a proof with existential variables still non-instantiated"
exception OpenProof of Names.Id.t option * open_error_reason
@@ -375,19 +369,25 @@ let _ = CErrors.register_handler begin function
| _ -> raise CErrors.Unhandled
end
+let warn_remaining_shelved_goals =
+ CWarnings.create ~name:"remaining-shelved-goals" ~category:"tactics"
+ (fun () -> Pp.str"The proof has remaining shelved goals")
+
+let warn_remaining_unresolved_evars =
+ CWarnings.create ~name:"remaining-unresolved-evars" ~category:"tactics"
+ (fun () -> Pp.str"The proof has unresolved variables")
+
let return ?pid (p : t) =
if not (is_done p) then
raise (OpenProof(pid, UnfinishedProof))
- else if has_shelved_goals p then
- raise (OpenProof(pid, HasShelvedGoals))
else if has_given_up_goals p then
raise (OpenProof(pid, HasGivenUpGoals))
- else if has_unresolved_evar p then
- (* spiwack: for compatibility with <= 8.3 proof engine *)
- raise (OpenProof(pid, HasUnresolvedEvar))
- else
+ else begin
+ if has_shelved_goals p then warn_remaining_shelved_goals ()
+ else if has_unresolved_evar p then warn_remaining_unresolved_evars ();
let p = unfocus end_of_stack_kind p () in
Proofview.return p.proofview
+ end
let compact p =
let entry, proofview = Proofview.compact p.entry p.proofview in
@@ -415,8 +415,9 @@ let run_tactic env tac pr =
Proofview.Unsafe.tclEVARS sigma >>= fun () ->
Proofview.tclUNIT retrieved
in
+ let { name; poly } = pr in
let (retrieved,proofview,(status,to_shelve,give_up),info_trace) =
- Proofview.apply env tac sp
+ Proofview.apply ~name ~poly env tac sp
in
let sigma = Proofview.return proofview in
let to_shelve = undef sigma to_shelve in
@@ -498,7 +499,8 @@ module V82 = struct
let sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) sigma in
Proofview.Unsafe.tclEVARS sigma
end in
- let ((), proofview, _, _) = Proofview.apply env tac pr.proofview in
+ let { name; poly } = pr in
+ let ((), proofview, _, _) = Proofview.apply ~name ~poly env tac pr.proofview in
let shelf =
List.filter begin fun g ->
Evd.is_undefined (Proofview.return proofview) g
diff --git a/proofs/proof.mli b/proofs/proof.mli
index fd5e905a3b..40e8ff7eef 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -130,13 +130,10 @@ val compact : t -> t
(* Returns the proofs (with their type) of the initial goals.
Raises [UnfinishedProof] is some goals remain to be considered.
Raises [HasShelvedGoals] if some goals are left on the shelf.
- Raises [HasGivenUpGoals] if some goals have been given up.
- Raises [HasUnresolvedEvar] if some evars have been left undefined. *)
+ Raises [HasGivenUpGoals] if some goals have been given up. *)
type open_error_reason =
| UnfinishedProof
- | HasShelvedGoals
| HasGivenUpGoals
- | HasUnresolvedEvar
exception OpenProof of Names.Id.t option * open_error_reason
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index f8adc58921..a47fa78f4d 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -22,51 +22,6 @@ open Names
module NamedDecl = Context.Named.Declaration
-(*** Proof Modes ***)
-
-(* Type of proof modes :
- - A function [set] to set it *from standard mode*
- - A function [reset] to reset the *standard mode* from it *)
-type proof_mode_name = string
-type proof_mode = {
- name : proof_mode_name ;
- set : unit -> unit ;
- reset : unit -> unit
-}
-
-let proof_modes = Hashtbl.create 6
-let find_proof_mode n =
- try Hashtbl.find proof_modes n
- with Not_found ->
- 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)
-
-(* initial mode: standard mode *)
-let standard = { name = "No" ; set = (fun ()->()) ; reset = (fun () -> ()) }
-let _ = register_proof_mode standard
-
-(* Default proof mode, to be set at the beginning of proofs. *)
-let default_proof_mode = ref (find_proof_mode "No")
-
-let get_default_proof_mode_name () =
- (CEphemeron.default !default_proof_mode standard).name
-
-let proof_mode_opt_name = ["Default";"Proof";"Mode"]
-let () =
- Goptions.(declare_string_option {
- optdepr = false;
- optname = "default proof mode" ;
- optkey = proof_mode_opt_name ;
- optread = begin fun () ->
- (CEphemeron.default !default_proof_mode standard).name
- end;
- optwrite = begin fun n ->
- default_proof_mode := find_proof_mode n
- end
- })
-
(*** Proof Global Environment ***)
(* Extra info on proofs. *)
@@ -95,7 +50,6 @@ type pstate = {
endline_tactic : Genarg.glob_generic_argument option;
section_vars : Constr.named_context option;
proof : Proof.t;
- mode : proof_mode CEphemeron.key;
universe_decl: UState.universe_decl;
strength : Decl_kinds.goal_kind;
}
@@ -109,29 +63,8 @@ let apply_terminator f = f
to be resumed when the current proof is closed or aborted. *)
let pstates = ref ([] : pstate list)
-(* Current proof_mode, for bookkeeping *)
-let current_proof_mode = ref !default_proof_mode
-
-(* combinators for proof modes *)
-let update_proof_mode () =
- match !pstates with
- | { mode = m } :: _ ->
- CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ());
- current_proof_mode := m;
- CEphemeron.iter_opt !current_proof_mode (fun x -> x.set ())
- | _ ->
- CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ());
- current_proof_mode := find_proof_mode "No"
-
(* combinators for the current_proof lists *)
-let push a l = l := a::!l;
- update_proof_mode ()
-
-exception NoSuchProof
-let () = CErrors.register_handler begin function
- | NoSuchProof -> CErrors.user_err Pp.(str "No such proof.")
- | _ -> raise CErrors.Unhandled
-end
+let push a l = l := a::!l
exception NoCurrentProof
let () = CErrors.register_handler begin function
@@ -152,6 +85,7 @@ let cur_pstate () =
let give_me_the_proof () = (cur_pstate ()).proof
let give_me_the_proof_opt () = try Some (give_me_the_proof ()) with | NoCurrentProof -> None
let get_current_proof_name () = (Proof.data (cur_pstate ()).proof).Proof.name
+let get_current_persistence () = (cur_pstate ()).strength
let with_current_proof f =
match !pstates with
@@ -221,25 +155,8 @@ let discard {CAst.loc;v=id} =
let discard_current () =
if List.is_empty !pstates then raise NoCurrentProof else pstates := List.tl !pstates
-
let discard_all () = pstates := []
-(* [set_proof_mode] sets the proof mode to be used after it's called. It is
- typically called by the Proof Mode command. *)
-let set_proof_mode m id =
- pstates := List.map
- (fun ps -> if pf_name_eq id ps then { ps with mode = m } else ps)
- !pstates;
- update_proof_mode ()
-
-let set_proof_mode mn =
- set_proof_mode (find_proof_mode mn) (get_current_proof_name ())
-
-let activate_proof_mode mode =
- CEphemeron.iter_opt (find_proof_mode mode) (fun x -> x.set ())
-let disactivate_current_proof_mode () =
- CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ())
-
(** [start_proof sigma id pl str goals terminator] starts a proof of name
[id] with goals [goals] (a list of pairs of environment and
conclusion); [str] describes what kind of theorem/definition this
@@ -254,9 +171,8 @@ let start_proof sigma name ?(pl=UState.default_univ_decl) kind goals terminator
proof = Proof.start ~name ~poly:(pi2 kind) sigma goals;
endline_tactic = None;
section_vars = None;
- mode = find_proof_mode "No";
- universe_decl = pl;
- strength = kind } in
+ strength = kind;
+ universe_decl = pl } in
push initial_state pstates
let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals terminator =
@@ -265,9 +181,8 @@ let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals termina
proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals;
endline_tactic = None;
section_vars = None;
- mode = find_proof_mode "No";
- universe_decl = pl;
- strength = kind } in
+ strength = kind;
+ universe_decl = pl } in
push initial_state pstates
let get_used_variables () = (cur_pstate ()).section_vars
@@ -353,7 +268,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
let used_univs_body = Vars.universes_of_constr body in
let used_univs_typ = Vars.universes_of_constr typ in
if allow_deferred then
- let initunivs = UState.const_univ_entry ~poly initial_euctx in
+ let initunivs = UState.univ_entry ~poly initial_euctx in
let ctx = constrain_variables universes in
(* For vi2vo compilation proofs are computed now but we need to
complement the univ constraints of the typ with the ones of
@@ -387,7 +302,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
else
fun t p ->
(* Already checked the univ_decl for the type universes when starting the proof. *)
- let univctx = Entries.Monomorphic_const_entry (UState.context_set universes) in
+ let univctx = UState.univ_entry ~poly:false universes in
let t = nf t in
Future.from_val (univctx, t),
Future.chain p (fun (pt,eff) ->
@@ -443,8 +358,13 @@ let return_proof ?(allow_partial=false) () =
(* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
side-effects... This may explain why one need to uniquize side-effects
thereafter... *)
+ let proof_opt c =
+ match EConstr.to_constr_opt evd c with
+ | Some p -> p
+ | None -> CErrors.user_err Pp.(str "Some unresolved existential variables remain")
+ in
let proofs =
- List.map (fun (c, _) -> (EConstr.to_constr evd c, eff)) initial_goals in
+ List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in
proofs, Evd.evar_universe_context evd
let close_future_proof ~opaque ~feedback_id proof =
@@ -461,19 +381,10 @@ let set_terminator hook =
| [] -> raise NoCurrentProof
| p :: ps -> pstates := { p with terminator = CEphemeron.create hook } :: ps
-module V82 = struct
- let get_current_initial_conclusions () =
- let { proof; strength } = cur_pstate () in
- let Proof.{ name; entry } = Proof.data proof in
- let initial = Proofview.initial_goals entry in
- let goals = List.map (fun (o, c) -> c) initial in
- name, (goals, strength)
-end
-
let freeze ~marshallable =
if marshallable then CErrors.anomaly (Pp.str"full marshalling of proof state not supported.")
else !pstates
-let unfreeze s = pstates := s; update_proof_mode ()
+let unfreeze s = pstates := s
let proof_of_state = function { proof }::_ -> proof | _ -> raise NoCurrentProof
let copy_terminators ~src ~tgt =
assert(List.length src = List.length tgt);
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index e762f3b7dc..38e234eaee 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -13,11 +13,11 @@
environment. *)
type t
-
val there_are_pending_proofs : unit -> bool
val check_no_pending_proof : unit -> unit
val get_current_proof_name : unit -> Names.Id.t
+val get_current_persistence : unit -> Decl_kinds.goal_kind
val get_all_proof_names : unit -> Names.Id.t list
val discard : Names.lident -> unit
@@ -105,8 +105,6 @@ val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t ->
val get_terminator : unit -> proof_terminator
val set_terminator : proof_terminator -> unit
-exception NoSuchProof
-
val get_open_goals : unit -> int
(** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is
@@ -130,56 +128,7 @@ val get_used_variables : unit -> Constr.named_context option
(** Get the universe declaration associated to the current proof. *)
val get_universe_decl : unit -> UState.universe_decl
-module V82 : sig
- val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list *
- Decl_kinds.goal_kind)
-end
-
val freeze : marshallable:bool -> t
val unfreeze : t -> unit
val proof_of_state : t -> Proof.t
val copy_terminators : src:t -> tgt:t -> t
-
-
-(**********************************************************)
-(* Proof Mode API *)
-(* The current Proof Mode API is deprecated and a new one *)
-(* will be (hopefully) defined in 8.8 *)
-(**********************************************************)
-
-(** Type of proof modes :
- - A name
- - A function [set] to set it *from standard mode*
- - A function [reset] to reset the *standard mode* from it
-
-*)
-type proof_mode_name = string
-type proof_mode = {
- name : proof_mode_name ;
- set : unit -> unit ;
- reset : unit -> unit
-}
-
-(** Registers a new proof mode which can then be adressed by name
- in [set_default_proof_mode].
- One mode is already registered - the standard mode - named "No",
- It corresponds to Coq default setting are they are set when coqtop starts. *)
-val register_proof_mode : proof_mode -> unit
-(* Can't make this deprecated due to limitations of camlp5 *)
-(* [@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] *)
-
-val proof_mode_opt_name : string list
-
-val get_default_proof_mode_name : unit -> proof_mode_name
-[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "]
-
-(** [set_proof_mode] sets the proof mode to be used after it's called. It is
- typically called by the Proof Mode command. *)
-val set_proof_mode : proof_mode_name -> unit
-[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "]
-
-val activate_proof_mode : proof_mode_name -> unit
-[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "]
-
-val disactivate_current_proof_mode : unit -> unit
-[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "]
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 1d796fece5..06e6b89df1 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -137,26 +137,6 @@ let refine ~typecheck f =
in
Proofview.Goal.enter (make_refine_enter ~typecheck f)
-(** Useful definitions *)
-
-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 env evd j t
- in
- evd , j'.Environ.uj_val
-
-let refine_casted ~typecheck f = Proofview.Goal.enter begin fun gl ->
- let concl = Proofview.Goal.concl gl in
- let env = Proofview.Goal.env gl in
- let f h =
- let (h, c) = f h in
- with_type env h c concl
- in
- refine ~typecheck f
-end
-
(** {7 solve_constraints}
Ensure no remaining unification problems are left. Run at every "." by default. *)
diff --git a/proofs/refine.mli b/proofs/refine.mli
index 1af6463a02..55dafe521f 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -34,17 +34,6 @@ val generic_refine : typecheck:bool -> ('a * EConstr.t) tactic ->
Proofview.Goal.t -> 'a tactic
(** The general version of refine. *)
-(** {7 Helper functions} *)
-
-val with_type : Environ.env -> Evd.evar_map ->
- EConstr.constr -> EConstr.types -> Evd.evar_map * EConstr.constr
-(** [with_type env sigma c t] ensures that [c] is of type [t]
- inserting a coercion if needed. *)
-
-val refine_casted : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic
-(** Like {!refine} except the refined term is coerced to the conclusion of the
- current goal. *)
-
(** {7 Unification constraint handling} *)
val solve_constraints : unit tactic
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 16:29:44 +0000