diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 8b8e41b34..128c2b265 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -143,3 +143,9 @@ val traverse : int -> unit val traverse_nth_goal : int -> unit val traverse_next_unproven : unit -> unit val traverse_prev_unproven : unit -> unit + + +(* These two functions make it possible to implement more elaborate + proof and goal management, as it is done, for instance in pcoq *) +val traverse_to : int list -> unit +val mutate : (pftreestate -> pftreestate) -> unit |