diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-15 18:30:46 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-15 18:30:46 +0000 |
| commit | b076264235980e60d51a5d0b8d3a4e9c3f4d82eb (patch) | |
| tree | 78a9d74850834a6fc4a413304ef6ec034e4763f2 /ide/coq.mli | |
| parent | 97c848795c1c26e6413737e9b8150eb9335946ed (diff) | |
Cleaned up a bit goal handling in Coqtop interface. Now we have two queries : goal description, with focused and unfocused goals, and list of currently declared evars.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14793 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coq.mli')
| -rw-r--r-- | ide/coq.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/ide/coq.mli b/ide/coq.mli index 5b5811392..662c6ccf2 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -49,7 +49,8 @@ val interp : coqtop -> ?raw:bool -> ?verbose:bool -> string -> string Interface.value val rewind : coqtop -> int -> int Interface.value val status : coqtop -> Interface.status Interface.value -val goals : coqtop -> Interface.goals Interface.value +val goals : coqtop -> Interface.goals option Interface.value +val evars : coqtop -> Interface.evar list option Interface.value val hints : coqtop -> (Interface.hint list * Interface.hint) option Interface.value val inloadpath : coqtop -> string -> bool Interface.value val mkcases : coqtop -> string -> string list list Interface.value |