From ab85be0ab41251ece3b583c3ff38f08f546f6414 Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Thu, 8 Aug 2013 18:52:29 +0000 Subject: Vernac classification streamlined (handles VERNAC EXTEND) The warning output by vernacextend when the classifier is missing is the documentation of this commit: Warning: Vernac entry "Foo" misses a classifier. A classifier is a function that returns an expression of type vernac_classification (see Vernacexpr). You can: - Use '... EXTEND Foo CLASSIFIED AS QUERY ...' if the new vernacular command does not alter the system state; - Use '... EXTEND Foo CLASSIFIED AS SIDEFF ...' if the new vernacular command alters the system state but not the parser nor it starts a proof or ends one; - Use '... EXTEND Foo CLASSIFIED BY f ...' to specify a global function f. The function f will be called passing "Foo" as the only argument; - Add a specific classifier in each clause using the syntax: '[...] => [ f ] -> [...]'. Specific classifiers have precedence over global classifiers. Only one classifier is called. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16680 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/toplevel.mllib | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'toplevel/toplevel.mllib') diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index d58df57f2..ab8c89623 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -19,9 +19,9 @@ Ppvernac Vernacinterp Mltop Vernacentries -Whelp Vernac_classifier Stm +Whelp Vernac Ide_slave Toplevel -- cgit v1.2.3