diff options
Diffstat (limited to 'proofs/proof.mli')
| -rw-r--r-- | proofs/proof.mli | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/proofs/proof.mli b/proofs/proof.mli index ff1253e7c..85b508447 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -49,6 +49,21 @@ val proof : proof -> * Goal.goal list * Evd.evar_map +(* Generic records structured like the return type of proof *) +type 'a pre_goals = { + fg_goals : 'a list; + (** List of the focussed goals *) + bg_goals : ('a list * 'a list) list; + (** Zipper representing the unfocussed background goals *) + shelved_goals : 'a list; + (** List of the goals on the shelf. *) + given_up_goals : 'a list; + (** List of the goals that have been given up *) +} + +val map_structured_proof : proof -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals) + + (*** General proof functions ***) val start : Evd.evar_map -> (Environ.env * Term.types) list -> proof |