diff options
| author |  bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-13 08:48:06 +0000 |
|---|---|---|
| committer | bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-13 08:48:06 +0000 |
| commit | 3bc2bb21ea017134ebd759062d71c932efb439e1 (patch) | |
| tree | 90bca77938fe9d385de9837d9c16d63149012678 /toplevel | |
| parent | fc507c51aba9e0258e41e3ea4c8b38bf2cc0dc1b (diff) | |
export a function that is needed in pcoq.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1372 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -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 801eb83eb..5efd2bd40 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;; |