diff options
| author | herbelin | 2003-10-08 12:37:03 +0000 |
|---|---|---|
| committer | herbelin | 2003-10-08 12:37:03 +0000 |
| commit | bd91698e1acdc5e579f904e3f52e40a57bd6cd13 (patch) | |
| tree | 0618b73cba5e1321ec6f1236f803e8c74cccf48b /proofs | |
| parent | f844897e7258db969e86f2e48e50e29ca5ec5802 (diff) | |
Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé incomplètement prouvé comme axiome
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4543 85f007b7-540e-0410-9357-904b9bb8a0f7
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 *) |