diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 5 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 6 |
2 files changed, 11 insertions, 0 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 4f8d8b07f2..7f8e748623 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -195,6 +195,11 @@ let cook_proof () = const_entry_opaque = true }, strength, ts.top_hook)) +let current_proof_statement () = + let ts = get_topstate() in + (get_current_proof_name (), ts.top_strength, + ts.top_goal.evar_concl, ts.top_hook) + (*********************************************************************) (* Abort functions *) (*********************************************************************) diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 9585e7b3c9..f4cc32a554 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -107,6 +107,7 @@ val set_xml_cook_proof : (pftreestate -> unit) -> unit val get_pftreestate : unit -> pftreestate (* [get_end_tac ()] returns the current tactic to apply to all new subgoal *) + val get_end_tac : unit -> tactic option (* [get_goal_context n] returns the context of the [n]th subgoal of @@ -119,6 +120,11 @@ val get_goal_context : int -> Evd.evar_map * env val get_current_goal_context : unit -> Evd.evar_map * env +(* [current_proof_statement] *) + +val current_proof_statement : + unit -> identifier * goal_kind * types * declaration_hook + (*s [get_current_proof_name ()] return the name of the current focused proof or failed if no proof is focused *) |