Achèvement nettoyage Pfedit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@421 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 3 deletions

diff --git a/lib/edit.mli b/lib/edit.mli
index 6d5744259d..5926456f0a 100644
--- a/lib/edit.mli
+++ b/lib/edit.mli
@@ -13,9 +13,11 @@ type ('a,'b,'c) t
 
 val empty : unit -> ('a,'b,'c) t
 
-(* sets the focus to the specified domain element, or if [None],
- * unsets the focus *)
-val focus : ('a,'b,'c) t -> 'a option -> unit
+(* sets the focus to the specified domain element *)
+val focus : ('a,'b,'c) t -> 'a -> unit
+
+(* unsets the focus which must not already be unfocused *)
+val unfocus : ('a,'b,'c) t -> unit
 
 (* gives the last focused element or [None] if none *)
 val last_focused : ('a,'b,'c) t -> 'a option