From ab915f905ca81018521db63cdd0f3126b35c69c6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 15 Oct 2017 19:21:00 +0200 Subject: [stm] First step to move interpretation of Undo commands out of the classifier. The vernacular classifier has a current special case for "Undo" like commands, as it needs access to the document structure in order to produce the proper "VtBack" classification, however the classifier is defined before the document is. We introduce a new delegation status `VtMeta` that allows us to interpreted such commands outside the classifier itself. --- stm/vernac_classifier.mli | 3 --- 1 file changed, 3 deletions(-) (limited to 'stm/vernac_classifier.mli') diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli index 2fa1e0b8d..fe42a03a3 100644 --- a/stm/vernac_classifier.mli +++ b/stm/vernac_classifier.mli @@ -18,9 +18,6 @@ val classify_vernac : vernac_expr -> vernac_classification 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 -- cgit v1.2.3