From 3bc2bb21ea017134ebd759062d71c932efb439e1 Mon Sep 17 00:00:00 2001
From: bertot
Date: Tue, 13 Feb 2001 08:48:06 +0000
Subject: 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
---
 toplevel/vernacentries.mli | 5 +++++
 1 file changed, 5 insertions(+)

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;;
-- 
cgit v1.2.3