diff options
Diffstat (limited to 'proofs/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 4f8d8b07f..7f8e74862 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 *) (*********************************************************************) |