Imported Upstream version 8.5~beta1+dfsg

1 files changed, 28 insertions, 0 deletions

diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli
new file mode 100644
index 00000000..0680fe84
--- /dev/null
+++ b/stm/vernac_classifier.mli
@@ -0,0 +1,28 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Vernacexpr
+open Genarg
+
+val string_of_vernac_classification : vernac_classification -> string
+
+(** What does a vernacular do *)
+val classify_vernac : vernac_expr -> vernac_classification
+
+(** Install a vernacular classifier for VernacExtend *)
+val declare_vernac_classifier :
+  Vernacexpr.extend_name -> (raw_generic_argument list -> unit -> vernac_classification) -> unit
+
+(** Set by Stm *)
+val set_undo_classifier : (vernac_expr -> vernac_classification) -> unit
+
+(** Standard constant classifiers *)
+val classify_as_query : vernac_classification
+val classify_as_sideeff : vernac_classification
+val classify_as_proofstep : vernac_classification
+