diff options
Diffstat (limited to 'proofs/pfedit.mli')
| -rw-r--r-- | proofs/pfedit.mli | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 2473af0c5b..7a953dff6e 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -6,7 +6,7 @@ open Pp open Sign open Declare open Proof_trees -open Refiner +open Tacmach (*i*) val proof_prompt : unit -> string @@ -32,3 +32,8 @@ val list_proofs : unit -> string list val add_proof : string * pftreestate * proof_topstate -> unit val del_proof : string -> unit val init_proofs : unit -> unit + +val make_focus : int -> unit +val focus : unit -> int +val focused_goal : unit -> int + |