From 1407a1caabd5891552043e9f62e5f2058df07034 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 26 Jul 2018 15:22:17 +0200
Subject: Document the coqpp implementation of VERNAC EXTEND.

---
 dev/doc/changes.md | 28 +++++++++++++++++++++++++++-
 1 file changed, 27 insertions(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index fdeb0abed4..157f41bd7b 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -159,7 +159,33 @@ END
 
 #### VERNAC EXTEND
 
-Not handled yet.
+Steps to perform:
+- replace the brackets enclosing OCaml code in actions and rule classifiers with
+  braces
+- if not there yet, add a leading `|̀  to the first rule
+
+Handwritten classifiers declared through the `CLASSIFIED BY` statement are
+considered OCaml code, so they also need to be wrapped in braces.
+
+All extension macros are now behaving as if they were declared `FUNCTIONAL`,
+which means that they must return an interpretation state. This should
+currently be done by merely returning the `st` variable that is implicitly
+passed to the rule code.
+
+For instance, code of the form:
+```
+VERNAC COMMAND EXTEND my_command CLASSIFIED BY classifier
+  [ "foo" int(i) ] => [ classif' ] -> [ cmd1 i ]
+| [ "bar" ] -> [ cmd2 ]
+END
+```
+should be turned into
+```
+VERNAC COMMAND EXTEND my_command CLASSIFIED BY { classifier }
+  [ "foo" int(i) ] => { classif' } -> { let () = cmd1 i in st }
+| [ "bar" ] -> { let () = cmd2 in st  }
+END
+```
 
 #### ARGUMENT EXTEND
 
-- 
cgit v1.2.3