From 3a4ba0659b7ed8072a7df5d2d978bf10194ff039 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 16 Jun 2016 12:00:22 +0200
Subject: COMMENTS: Vernacexpr.extend_name

---
 intf/vernacexpr.mli | 27 ++++++++++++++++++++++++++-
 1 file changed, 26 insertions(+), 1 deletion(-)

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 1c75d76dd5..156e00368d 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -232,7 +232,32 @@ type section_subset_expr =
   | SsSubstr of section_subset_expr * section_subset_expr
   | SsFwdClose of section_subset_expr
 
-(** Extension identifiers for the VERNAC EXTEND mechanism. *)
+(** Extension identifiers for the VERNAC EXTEND mechanism.
+
+    {b ("Extraction", 0} indicates {b Extraction {i qualid}} command.
+
+    {b ("Extraction", 1} indicates {b Recursive Extraction {i qualid}} command.
+
+    {b ("Extraction", 2)} indicates {b Extraction "{i filename}" {i qualid{_ 1}} ... {i qualid{_ n}}} command.
+
+    {b ("ExtractionLibrary", 0)} indicates {b Extraction Library {i ident}} command.
+
+    {b ("RecursiveExtractionLibrary", 0)} indicates {b Recursive Extraction Library {i ident}} command.
+
+    {b ("SeparateExtraction", 0)} indicates {b Separate Extraction {i qualid{_ 1}} ... {i qualid{_ n}}} command.
+
+    {b ("ExtractionLanguage", 0)} indicates {b Extraction Language Ocaml} or {b Extraction Language Haskell} or {b Extraction Language Scheme} or {b Extraction Language JSON} commands.
+
+    {b ("ExtractionImplicit", 0)} indicates {b Extraction Implicit {i qualid} \[ {i ident{_1}} ... {i ident{_n} } \] } command.
+
+    {b ("ExtractionConstant", 0)} indicates {b Extract Constant {i qualid} => {i string}} command.
+
+    {b ("ExtractionInlinedConstant", 0)} indicates {b Extract Inlined Constant {i qualid} => {i string}} command.
+
+    {b ("ExtractionInductive", 0)} indicates {b Extract Inductive {i qualid} => {i string} [ {i string} ... {string} ] {i optstring}} command.
+
+    {b ("ExtractionBlacklist", 0)} indicates {b Extraction Blacklist {i ident{_1}} ... {i ident{_n}}} command.
+ *)
 type extend_name =
   (** Name of the vernac entry where the tactic is defined, typically found
       after the VERNAC EXTEND statement in the source. *)
-- 
cgit v1.2.3