aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/funind/functional_principles_proofs.ml2
-rw-r--r--plugins/funind/indfun_common.ml5
-rw-r--r--plugins/funind/indfun_common.mli6
-rw-r--r--plugins/funind/invfun.ml2
-rw-r--r--plugins/funind/recdef.ml18
-rw-r--r--proofs/pfedit.ml21
-rw-r--r--proofs/pfedit.mli16
-rw-r--r--proofs/proof_global.ml45
-rw-r--r--proofs/proof_global.mli31
-rw-r--r--toplevel/lemmas.ml108
-rw-r--r--toplevel/lemmas.mli28
-rw-r--r--toplevel/stm.ml2
-rw-r--r--toplevel/vernacentries.ml15
13 files changed, 160 insertions, 139 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 52ba41869a..f4e8589031 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -983,7 +983,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
lemma_type
(fun _ _ -> ());
ignore (Pfedit.by (Proofview.V82.tactic prove_replacement));
- Lemmas.save_named false
+ Lemmas.save_proof (Vernacexpr.Proved(false,None))
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index b7072ea3bd..db4297b37d 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -169,11 +169,6 @@ let cook_proof _ =
let (id,(entry,_,strength,hook)) = Pfedit.cook_proof (fun _ -> ()) in
(id,(entry,strength,hook))
-let new_save_named opacity =
- let id,(const,persistence,hook) = cook_proof true in
- let const = { const with const_entry_opaque = opacity } in
- save true id const persistence hook
-
let get_proof_clean do_reduce =
let result = cook_proof do_reduce in
Pfedit.delete_current_proof ();
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 722f857b34..cea5ffe259 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -46,12 +46,6 @@ val const_of_id: Id.t -> constant
val jmeq : unit -> Term.constr
val jmeq_refl : unit -> Term.constr
-(* [save_named] is a copy of [Command.save_named] but uses
- [nf_betaiotazeta] instead of [nf_betaiotaevar_preserving_vm_cast]
-*)
-
-val new_save_named : bool -> unit
-
val save : bool -> Id.t -> Entries.definition_entry -> Decl_kinds.goal_kind ->
unit Tacexpr.declaration_hook Ephemeron.key -> unit
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 0d32bf2bc9..7c8f5714e6 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1008,7 +1008,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
-let do_save () = Lemmas.save_named false
+let do_save () = Lemmas.save_proof (Vernacexpr.Proved(false,None))
(* [derive_correctness make_scheme functional_induction funs graphs] create correctness and completeness
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 6afbff779d..082d7ad51e 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -64,7 +64,7 @@ let (declare_fun : Id.t -> logical_kind -> constr -> global_reference) =
const_entry_inline_code = false} in
ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
-let defined () = Lemmas.save_named false
+let defined () = Lemmas.save_proof (Vernacexpr.Proved (false,None))
let def_of_const t =
match (kind_of_term t) with
@@ -1249,7 +1249,6 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
with e when Errors.noncritical e ->
anomaly (Pp.str "open_new_goal with an unamed theorem")
in
- let sign = initialize_named_context_for_proof () in
let na = next_global_ident_away name [] in
if Termops.occur_existential gls_type then
Errors.error "\"abstract\" cannot handle existentials";
@@ -1309,12 +1308,11 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
)
g)
;
- Lemmas.save_named opacity;
+ Lemmas.save_proof (Vernacexpr.Proved(opacity,None));
in
- start_proof
+ Lemmas.start_proof
na
(Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma)
- sign
gls_type
hook;
if Indfun_common.is_strict_tcc ()
@@ -1360,8 +1358,8 @@ let com_terminate
hook =
let start_proof (tac_start:tactic) (tac_end:tactic) =
let (evmap, env) = Lemmas.get_current_context() in
- start_proof thm_name
- (Global, Proof Lemma) (Environ.named_context_val env)
+ Lemmas.start_proof thm_name
+ (Global, Proof Lemma) ~sign:(Environ.named_context_val env)
(compute_terminate_type nb_args fonctional_ref) hook;
ignore (by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start)));
@@ -1408,8 +1406,8 @@ let (com_eqn : int -> Id.t ->
let (evmap, env) = Lemmas.get_current_context() in
let f_constr = constr_of_global f_ref in
let equation_lemma_type = subst1 f_constr equation_lemma_type in
- (start_proof eq_name (Global, Proof Lemma)
- (Environ.named_context_val env) equation_lemma_type (fun _ _ -> ());
+ (Lemmas.start_proof eq_name (Global, Proof Lemma)
+ ~sign:(Environ.named_context_val env) equation_lemma_type (fun _ _ -> ());
ignore (by
(Proofview.V82.tactic (start_equation f_ref terminate_ref
(fun x ->
@@ -1440,7 +1438,7 @@ let (com_eqn : int -> Id.t ->
)));
(* (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *)
(* Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *)
- Flags.silently (fun () -> Lemmas.save_named opacity) () ;
+ Flags.silently (fun () -> Lemmas.save_proof (Vernacexpr.Proved(opacity,None))) () ;
(* Pp.msgnl (str "eqn finished"); *)
);;
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 8a52244df2..e4cdf49896 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -29,9 +29,9 @@ let delete_all_proofs = Proof_global.discard_all
let set_undo _ = ()
let get_undo _ = None
-let start_proof (id : Id.t) str hyps c ?init_tac ?compute_guard hook =
+let start_proof (id : Id.t) str hyps c ?init_tac ?compute_guard hook terminator =
let goals = [ (Global.env_of_context hyps , c) ] in
- Proof_global.start_proof id str goals ?compute_guard hook;
+ Proof_global.start_proof id str goals ?compute_guard hook terminator;
let env = Global.env () in
ignore (Proof_global.with_current_proof (fun _ p ->
match init_tac with
@@ -40,11 +40,12 @@ let start_proof (id : Id.t) str hyps c ?init_tac ?compute_guard hook =
let cook_this_proof hook p =
match p with
- | (i,([e],cg,str,h)) -> (i,(e,cg,str,h))
+ | { Proof_global.id;entries=[constr];do_guard;persistence;hook } ->
+ (id,(constr,do_guard,persistence,hook))
| _ -> Errors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.")
let cook_proof hook =
- cook_this_proof hook (Proof_global.close_proof (fun x -> x))
+ cook_this_proof hook (fst (Proof_global.close_proof (fun x -> x)))
let get_pftreestate () =
Proof_global.give_me_the_proof ()
@@ -122,7 +123,7 @@ open Decl_kinds
let next = let n = ref 0 in fun () -> incr n; !n
let build_constant_by_tactic id sign ?(goal_kind = Global,Proof Theorem) typ tac =
- start_proof id goal_kind sign typ (fun _ _ -> ());
+ start_proof id goal_kind sign typ (fun _ _ -> ()) (fun _ -> ());
try
let status = by tac in
let _,(const,_,_,_) = cook_proof (fun _ -> ()) in
@@ -166,13 +167,3 @@ let solve_by_implicit_tactic env sigma evk =
(try fst (build_by_tactic env evi.evar_concl (Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) [])))
with e when Logic.catchable_exception e -> raise Exit)
| _ -> raise Exit
-
-
-
-
-
-
-
-
-
-
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 6dad738afb..110df23470 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -62,7 +62,7 @@ type lemma_possible_guards = Proof_global.lemma_possible_guards
val start_proof :
Id.t -> goal_kind -> named_context_val -> constr ->
?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards ->
- unit declaration_hook -> unit
+ unit declaration_hook -> Proof_global.proof_terminator -> unit
(** {6 ... } *)
(** [cook_proof opacity] turns the current proof (assumed completed) into
@@ -71,19 +71,15 @@ val start_proof :
it also tells if the guardness condition has to be inferred. *)
val cook_this_proof : (Proof.proof -> unit) ->
- Id.t *
- (Entries.definition_entry list *
- lemma_possible_guards *
- Decl_kinds.goal_kind *
- unit Tacexpr.declaration_hook Ephemeron.key) ->
- Id.t *
+ Proof_global.proof_object ->
+ (Id.t *
(Entries.definition_entry * lemma_possible_guards * goal_kind *
- unit declaration_hook Ephemeron.key)
+ unit declaration_hook Ephemeron.key))
val cook_proof : (Proof.proof -> unit) ->
- Id.t *
+ (Id.t *
(Entries.definition_entry * lemma_possible_guards * goal_kind *
- unit declaration_hook Ephemeron.key)
+ unit declaration_hook Ephemeron.key))
(** {6 ... } *)
(** [get_pftreestate ()] returns the current focused pending proof.
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index b7a32a9801..b2282a6831 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -65,14 +65,28 @@ let _ =
(* Extra info on proofs. *)
type lemma_possible_guards = int list list
+type proof_object = {
+ id : Names.Id.t;
+ entries : Entries.definition_entry list;
+ do_guard : lemma_possible_guards;
+ persistence : Decl_kinds.goal_kind;
+ hook : unit Tacexpr.declaration_hook Ephemeron.key
+}
+
+type proof_ending = Vernacexpr.proof_end * proof_object
+type proof_terminator =
+ proof_ending -> unit
+type closed_proof = proof_object*proof_terminator Ephemeron.key
+
type pstate = {
pid : Id.t;
+ terminator : proof_terminator Ephemeron.key;
endline_tactic : Tacexpr.raw_tactic_expr option;
section_vars : Context.section_context option;
proof : Proof.proof;
strength : Decl_kinds.goal_kind;
compute_guard : lemma_possible_guards;
- hook : unit Tacexpr.declaration_hook Ephemeron.key;
+ pr_hook : unit Tacexpr.declaration_hook Ephemeron.key;
mode : proof_mode Ephemeron.key;
}
@@ -236,27 +250,29 @@ end
It raises exception [ProofInProgress] if there is a proof being
currently edited. *)
-let start_proof id str goals ?(compute_guard=[]) hook =
+let start_proof id str goals ?(compute_guard=[]) hook terminator =
let initial_state = {
pid = id;
+ terminator = Ephemeron.create terminator;
proof = Proof.start Evd.empty goals;
endline_tactic = None;
section_vars = None;
strength = str;
compute_guard = compute_guard;
- hook = Ephemeron.create hook;
+ pr_hook = Ephemeron.create hook;
mode = find_proof_mode "No" } in
push initial_state pstates
-let start_dependent_proof id str goals ?(compute_guard=[]) hook =
+let start_dependent_proof id str goals ?(compute_guard=[]) hook terminator =
let initial_state = {
pid = id;
+ terminator = Ephemeron.create terminator;
proof = Proof.dependent_start Evd.empty goals;
endline_tactic = None;
section_vars = None;
strength = str;
compute_guard = compute_guard;
- hook = Ephemeron.create hook;
+ pr_hook = Ephemeron.create hook;
mode = find_proof_mode "No" } in
push initial_state pstates
@@ -280,13 +296,10 @@ let get_open_goals () =
(List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) +
List.length shelf
-type closed_proof =
- Names.Id.t *
- (Entries.definition_entry list * lemma_possible_guards *
- Decl_kinds.goal_kind * unit Tacexpr.declaration_hook Ephemeron.key)
-
let close_proof ~now fpl =
- let { pid;section_vars;compute_guard;strength;hook;proof } = cur_pstate () in
+ let { pid;section_vars;compute_guard;strength;pr_hook;proof;terminator } =
+ cur_pstate ()
+ in
let initial_goals = Proof.initial_goals proof in
let entries = Future.map2 (fun p (c, t) -> { Entries.
const_entry_body = p;
@@ -296,7 +309,11 @@ let close_proof ~now fpl =
const_entry_opaque = true }) fpl initial_goals in
if now then
List.iter (fun x -> ignore(Future.join x.Entries.const_entry_body)) entries;
- (pid, (entries, compute_guard, strength, hook))
+ { id = pid ;
+ entries = entries ;
+ do_guard = compute_guard ;
+ persistence = strength ;
+ hook = pr_hook } , terminator
let return_proof () =
let { proof } = cur_pstate () in
@@ -471,8 +488,8 @@ let _ =
module V82 = struct
let get_current_initial_conclusions () =
- let { pid; strength; hook; proof } = cur_pstate () in
- pid, (List.map snd (Proof.initial_goals proof), strength, hook)
+ let { pid; strength; pr_hook; proof } = cur_pstate () in
+ pid, (List.map snd (Proof.initial_goals proof), strength, pr_hook)
end
type state = pstate list
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index e88c2f3942..eb7d0ecb17 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -46,17 +46,37 @@ exception NoCurrentProof
val give_me_the_proof : unit -> Proof.proof
(** @raise NoCurrentProof when outside proof mode. *)
+(** When a proof is closed, it is reified into a [proof_object], where
+ [id] is the name of the proof, [entries] the list of the proof terms
+ (in a form suitable for definitions). Together with the [terminator]
+ function which takes a [proof_object] together with a [proof_end]
+ (i.e. an proof ending command) and registers the appropriate
+ values. *)
+type lemma_possible_guards = int list list
+type proof_object = {
+ id : Names.Id.t;
+ entries : Entries.definition_entry list;
+ do_guard : lemma_possible_guards;
+ persistence : Decl_kinds.goal_kind;
+ hook : unit Tacexpr.declaration_hook Ephemeron.key
+}
+
+type proof_ending = Vernacexpr.proof_end * proof_object
+type proof_terminator =
+ proof_ending -> unit
+type closed_proof = proof_object*proof_terminator Ephemeron.key
+
(** [start_proof s str goals ~init_tac ~compute_guard hook] starts
a proof of name [s] and
conclusion [t]; [hook] is optionally a function to be applied at
proof end (e.g. to declare the built constructions as a coercion
or a setoid morphism). *)
-type lemma_possible_guards = int list list
val start_proof : Names.Id.t ->
Decl_kinds.goal_kind ->
(Environ.env * Term.types) list ->
- ?compute_guard:lemma_possible_guards ->
- unit Tacexpr.declaration_hook ->
+ ?compute_guard:lemma_possible_guards ->
+ unit Tacexpr.declaration_hook ->
+ proof_terminator ->
unit
(** Like [start_proof] except that there may be dependencies between
initial goals. *)
@@ -65,12 +85,9 @@ val start_dependent_proof : Names.Id.t ->
Proofview.telescope ->
?compute_guard:lemma_possible_guards ->
unit Tacexpr.declaration_hook ->
+ proof_terminator ->
unit
-type closed_proof =
- Names.Id.t *
- (Entries.definition_entry list * lemma_possible_guards *
- Decl_kinds.goal_kind * unit Tacexpr.declaration_hook Ephemeron.key)
(* Takes a function to add to the exceptions data relative to the
state in which the proof was built *)
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 20b792cc07..db479615ef 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -169,7 +169,7 @@ let look_for_possibly_mutual_statements = function
(* Saving a goal *)
-let save ?proof id const do_guard (locality,kind) hook =
+let save id const do_guard (locality,kind) hook =
let const = adjust_guardness_conditions const do_guard in
let k = Kindops.logical_kind_of_goal_kind kind in
let l,r = match locality with
@@ -185,8 +185,6 @@ let save ?proof id const do_guard (locality,kind) hook =
let kn = declare_constant id ~local (DefinitionEntry const, k) in
Autoinstance.search_declaration (ConstRef kn);
(locality, ConstRef kn) in
- (* if the proof is given explicitly, nothing has to be deleted *)
- if Option.is_empty proof then Pfedit.delete_current_proof ();
definition_message id;
Ephemeron.iter_opt hook (fun f -> f l r)
@@ -260,42 +258,75 @@ let save_remaining_recthms (locality,kind) body opaq i (id,(t_i,(_,imps))) =
let save_hook = ref ignore
let set_save_hook f = save_hook := f
-let get_proof ?proof opacity =
- let id,(const,do_guard,persistence,hook) =
- match proof with
- | None -> Pfedit.cook_proof !save_hook
- | Some p -> Pfedit.cook_this_proof !save_hook p in
- id,{const with const_entry_opaque = opacity},do_guard,persistence,hook
-
-let save_named ?proof opacity =
- let id,const,do_guard,persistence,hook = get_proof ?proof opacity in
- save ?proof id const do_guard persistence hook
+let save_named proof =
+ let id,const,do_guard,persistence,hook = proof in
+ save id const do_guard persistence hook
let check_anonymity id save_ident =
if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then
error "This command can only be used for unnamed theorem."
-let save_anonymous ?proof opacity save_ident =
- let id,const,do_guard,persistence,hook = get_proof ?proof opacity in
+let save_anonymous proof save_ident =
+ let id,const,do_guard,persistence,hook = proof in
check_anonymity id save_ident;
- save ?proof save_ident const do_guard persistence hook
+ save save_ident const do_guard persistence hook
-let save_anonymous_with_strength ?proof kind opacity save_ident =
- let id,const,do_guard,_,hook = get_proof ?proof opacity in
+let save_anonymous_with_strength proof kind save_ident =
+ let id,const,do_guard,_,hook = proof in
check_anonymity id save_ident;
(* we consider that non opaque behaves as local for discharge *)
- save ?proof save_ident const do_guard (Global, Proof kind) hook
+ save save_ident const do_guard (Global, Proof kind) hook
+
+(* Admitted *)
+
+let admit () =
+ let (id,k,typ,hook) = Pfedit.current_proof_statement () in
+ let e = Pfedit.get_used_variables(), typ, None in
+ let kn = declare_constant id (ParameterEntry e,IsAssumption Conjectural) in
+ let () = match fst k with
+ | Global -> ()
+ | Local | Discharge ->
+ msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++
+ str "declared as an axiom.")
+ in
+ let () = assumption_message id in
+ Ephemeron.iter_opt hook (fun f -> f Global (ConstRef kn))
(* Starting a goal *)
let start_hook = ref ignore
let set_start_hook = (:=) start_hook
-let start_proof id kind c ?init_tac ?(compute_guard=[]) hook =
- let sign = initialize_named_context_for_proof () in
+
+let get_proof proof opacity =
+ let (id,(const,do_guard,persistence,hook)) =
+ Pfedit.cook_this_proof !save_hook proof
+ in
+ id,{const with const_entry_opaque = opacity},do_guard,persistence,hook
+
+let start_proof id kind ?sign c ?init_tac ?(compute_guard=[]) hook =
+ let terminator = let open Vernacexpr in function
+ | Admitted,_ ->
+ admit ();
+ Pp.feedback Interface.AddedAxiom
+ | Proved (is_opaque,idopt),proof ->
+ let proof = get_proof proof is_opaque in
+ begin match idopt with
+ | None -> save_named proof
+ | Some ((_,id),None) -> save_anonymous proof id
+ | Some ((_,id),Some kind) ->
+ save_anonymous_with_strength proof kind id
+ end
+ in
+ let sign =
+ match sign with
+ | Some sign -> sign
+ | None -> initialize_named_context_for_proof ()
+ in
!start_hook c;
- Pfedit.start_proof id kind sign c ?init_tac ~compute_guard hook
+ Pfedit.start_proof id kind sign c ?init_tac ~compute_guard hook terminator
+
let rec_tac_initializer finite guard thms snl =
if finite then
@@ -365,21 +396,18 @@ let start_proof_com kind thms hook =
let recguard,thms,snl = look_for_possibly_mutual_statements thms in
start_proof_with_initialization kind recguard thms snl hook
-(* Admitted *)
-let admit () =
- let (id,k,typ,hook) = Pfedit.current_proof_statement () in
- let e = Pfedit.get_used_variables(), typ, None in
- let kn = declare_constant id (ParameterEntry e,IsAssumption Conjectural) in
- let () = Pfedit.delete_current_proof () in
- let () = match fst k with
- | Global -> ()
- | Local | Discharge ->
- msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++
- str "declared as an axiom.")
+(* Saving a proof *)
+
+let save_proof ?proof ending =
+ let (proof_obj,terminator) =
+ match proof with
+ | None -> Proof_global.close_proof (fun x -> x)
+ | Some proof -> proof
in
- let () = assumption_message id in
- Ephemeron.iter_opt hook (fun f -> f Global (ConstRef kn))
+ (* if the proof is given explicitly, nothing has to be deleted *)
+ if Option.is_empty proof then Pfedit.delete_current_proof ();
+ Ephemeron.get terminator (ending,proof_obj)
(* Miscellaneous *)
@@ -387,3 +415,13 @@ let get_current_context () =
try Pfedit.get_current_goal_context ()
with e when Logic.catchable_exception e ->
(Evd.empty, Global.env())
+
+
+
+
+
+
+
+
+
+
diff --git a/toplevel/lemmas.mli b/toplevel/lemmas.mli
index 25e5a44304..65efff271f 100644
--- a/toplevel/lemmas.mli
+++ b/toplevel/lemmas.mli
@@ -18,7 +18,7 @@ open Pfedit
(** A hook start_proof calls on the type of the definition being started *)
val set_start_hook : (types -> unit) -> unit
-val start_proof : Id.t -> goal_kind -> types ->
+val start_proof : Id.t -> goal_kind -> ?sign:Environ.named_context_val -> types ->
?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards ->
unit declaration_hook -> unit
@@ -31,35 +31,17 @@ val start_proof_with_initialization :
(Id.t * (types * (Name.t list * Impargs.manual_explicitation list))) list
-> int list option -> unit declaration_hook -> unit
-(** A hook the next three functions pass to cook_proof *)
-val set_save_hook : (Proof.proof -> unit) -> unit
-
(** {6 ... } *)
-(** [save_named b] saves the current completed (or the provided) proof
- under the name it was started; boolean [b] tells if the theorem is
- declared opaque; it fails if the proof is not completed *)
-
-val save_named : ?proof:Proof_global.closed_proof -> bool -> unit
-
-(** [save_anonymous b name] behaves as [save_named] but declares the theorem
-under the name [name] and respects the strength of the declaration *)
-val save_anonymous :
- ?proof:Proof_global.closed_proof -> bool -> Id.t -> unit
-
-(** [save_anonymous_with_strength s b name] behaves as [save_anonymous] but
- declares the theorem under the name [name] and gives it the
- strength [strength] *)
-
-val save_anonymous_with_strength :
- ?proof:Proof_global.closed_proof -> theorem_kind -> bool -> Id.t -> unit
+(** A hook the next three functions pass to cook_proof *)
+val set_save_hook : (Proof.proof -> unit) -> unit
-(** [admit ()] aborts the current goal and save it as an assmumption *)
+val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit
-val admit : unit -> unit
(** [get_current_context ()] returns the evar context and env of the
current open proof if any, otherwise returns the empty evar context
and the current global env *)
val get_current_context : unit -> Evd.evar_map * Environ.env
+
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index d8f9052563..de0ece06d3 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -1805,7 +1805,7 @@ let show_script ?proof () =
let prf =
match proof with
| None -> Pfedit.get_current_proof_name ()
- | Some (id,_) -> id in
+ | Some (p,_) -> p.Proof_global.id in
let cmds = get_script prf in
let _,_,_,indented_cmds =
List.fold_left indent_script_item ((1,[]),false,[],[]) cmds
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d5e6ff1907..db51ff6103 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -457,17 +457,10 @@ let qed_display_script = ref true
let show_script = ref (fun ?proof () -> ())
let vernac_end_proof ?proof = function
- | Admitted ->
- admit ();
- Pp.feedback Interface.AddedAxiom
- | Proved (is_opaque,idopt) ->
+ | Admitted -> save_proof ?proof Admitted
+ | Proved (_,_) as e ->
if is_verbose () && !qed_display_script then !show_script ?proof ();
- begin match idopt with
- | None -> save_named ?proof is_opaque
- | Some ((_,id),None) -> save_anonymous ?proof is_opaque id
- | Some ((_,id),Some kind) ->
- save_anonymous_with_strength ?proof kind is_opaque id
- end
+ save_proof ?proof e
(* A stupid macro that should be replaced by ``Exact c. Save.'' all along
the theories [??] *)
@@ -476,7 +469,7 @@ let vernac_exact_proof c =
(* spiwack: for simplicity I do not enforce that "Proof proof_term" is
called only at the begining of a proof. *)
let status = by (Tactics.New.exact_proof c) in
- save_named true;
+ save_proof (Vernacexpr.Proved(true,None));
if not status then Pp.feedback Interface.AddedAxiom
let vernac_assumption locality (local, kind) l nl =
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 23:36:49 +0000