diff options
Diffstat (limited to 'toplevel/interface.mli')
| -rw-r--r-- | toplevel/interface.mli | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/toplevel/interface.mli b/toplevel/interface.mli index f3374ab4..39fb2a0e 100644 --- a/toplevel/interface.mli +++ b/toplevel/interface.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -29,17 +29,23 @@ type evar = { } type status = { - status_path : string option; + status_path : string list; (** Module path of the current proof *) status_proofname : string option; - (** Current proof name. [None] if no proof is in progress *) + (** Current proof name. [None] if no focussed proof is in progress *) + status_allproofs : string list; + (** List of all pending proofs. Order is not significant *) + status_statenum : int; + (** A unique id describing the state of coqtop *) + status_proofnum : int; + (** An id describing the state of the current proof. *) } type goals = { fg_goals : goal list; (** List of the focussed goals *) - bg_goals : goal list; - (** List of the background goals *) + bg_goals : (goal list * goal list) list; + (** Zipper representing the unfocussed background goals *) } type hint = (string * string) list |