diff options
Diffstat (limited to 'lib/interface.mli')
| -rw-r--r-- | lib/interface.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/interface.mli b/lib/interface.mli index d190272569..31577e6296 100644 --- a/lib/interface.mli +++ b/lib/interface.mli @@ -46,6 +46,8 @@ type goals = { (** Zipper representing the unfocussed background goals *) shelved_goals : goal list; (** List of the goals on the shelf. *) + given_up_goals : goal list; + (** List of the goals that have been given up *) } type hint = (string * string) list |