From 752d4bd4c19bdfe427d2ab033ac18674a91faa25 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 1 Dec 1999 10:50:05 +0000
Subject: module Pfedit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@169 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/pfedit.mli | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'proofs/pfedit.mli')

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
+
-- 
cgit v1.2.3