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 /plugins/decl_mode/decl_mode.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 'plugins/decl_mode/decl_mode.mli')
| -rw-r--r-- | plugins/decl_mode/decl_mode.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli index 72c46c7e7d..4e636598f9 100644 --- a/plugins/decl_mode/decl_mode.mli +++ b/plugins/decl_mode/decl_mode.mli @@ -70,3 +70,9 @@ val get_stack : Proof.proof -> stack_info list val get_top_stack : Proof.proof -> stack_info list val get_last: Environ.env -> identifier + +val focus : Proof.proof -> unit + +val unfocus : Proof.proof -> unit + +val maximal_unfocus : Proof.proof -> unit |