diff options
| -rw-r--r-- | toplevel/vernacentries.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index 801eb83eb4..5efd2bd40a 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -31,3 +31,8 @@ val global : Coqast.loc -> qualid -> global_reference;; (* this function is used to analyse the extra arguments in search commands. It is used in pcoq. *) val inside_outside : vernac_arg list -> dir_path list * bool;; + +(* This function makes sure that the function given is argument is preceded + by a command aborting all proofs if necessary. + It is used in pcoq. *) +val abort_refine : ('a -> unit) -> 'a -> unit;; |