diff options
| author | aspiwack | 2011-02-10 10:10:58 +0000 |
|---|---|---|
| committer | aspiwack | 2011-02-10 10:10:58 +0000 |
| commit | ac776b4660e95577eb6742200d882b8cf683cc10 (patch) | |
| tree | 40cd96020ddd0a3f23f2580c2921d27001186161 /proofs/proof.mli | |
| parent | daf397883f9b7f79eeddc6cc4580ecdc5ec793f5 (diff) | |
Started to fix the declarative proof mode (C-zar).
Everything seems to work fine in CoqIDE (except escape/return and the daimon which are not entirely ported).
However, there is some problem causing proof general to fail when using goto or evaluate buffer (evaluate next phrase works fine though), as well as coqc.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13817 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/proof.mli')
| -rw-r--r-- | proofs/proof.mli | 36 |
1 files changed, 24 insertions, 12 deletions
diff --git a/proofs/proof.mli b/proofs/proof.mli index ab1c0b8345..bb651dea11 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -64,32 +64,44 @@ val add_undo : (unit -> unit) -> proof -> unit (*** Focusing actions ***) -(* [focus_kind] is the type used by focusing and unfocusing +(* ['a focus_kind] is the type used by focusing and unfocusing commands to synchronise. Focusing and unfocusing commands use - a particular focus_kind, and if they don't match, the unfocusing command - will fail. *) -type focus_kind -val new_focus_kind : unit -> focus_kind + a particular ['a focus_kind], and if they don't match, the unfocusing command + will fail. + When focusing with an ['a focus_kind], an information of type ['a] is + stored at the focusing point. An example use is the "induction" tactic + of the declarative mode where sub-tactics must be aware of the current + induction argument. *) +type 'a focus_kind +val new_focus_kind : unit -> 'a focus_kind (* To be authorized to unfocus one must meet the condition prescribed by - the action which focused.*) -type focus_condition + the action which focused. + Conditions always carry a focus kind, and inherit their type parameter + from it.*) +type 'a focus_condition (* [no_cond] only checks that the unfocusing command uses the right [focus_kind]. *) -val no_cond : focus_kind -> focus_condition +val no_cond : 'a focus_kind -> 'a focus_condition (* [done_cond] checks that the unfocusing command uses the right [focus_kind] and that the focused proofview is complete. *) -val done_cond : focus_kind -> focus_condition +val done_cond : 'a focus_kind -> 'a focus_condition (* focus command (focuses on the [i]th subgoal) *) -(* there could also, easily be a focus-on-a-range tactic, is there +(* spiwack: there could also, easily be a focus-on-a-range tactic, is there a need for it? *) -val focus : focus_condition -> int -> proof -> unit +val focus : 'a focus_condition -> 'a -> int -> proof -> unit exception FullyUnfocused (* Unfocusing command. Raises [FullyUnfocused] if the proof is not focused. *) -val unfocus : focus_kind -> proof -> unit +val unfocus : 'a focus_kind -> proof -> unit + +(* [get_at_focus k] gets the information stored at the closest focus point + of kind [k]. + Raises [NoSuchFocus] if there is no focus point of kind [k]. *) +exception NoSuchFocus +val get_at_focus : 'a focus_kind -> proof -> 'a (* returns [true] if there is no goal under focus. *) val no_focused_goal : proof -> bool |