From 6b5b4db599333546334bcdbd852be72ddb39d9dc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 11 Oct 2018 18:13:12 +0200
Subject: Deprecating the RAW_TYPED and GLOB_TYPED stanzas of the ARGUMENT
 EXTEND macro.

Those optional arguments did not really make sense. It was pretty clear from
our code base, as all instances where triplicating the same type for TYPED,
RAW_TYPED and GLOB_TYPED.
---
 dev/doc/changes.md | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'dev/doc/changes.md')

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index f30b4107b6..c5632411d1 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -27,6 +27,11 @@ Coqlib:
   command then enables to locate the registered constant through its name. The
   name resolution is dynamic.
 
+Macros:
+
+- The RAW_TYPED AS and GLOB_TYPED AS stanzas of the ARGUMENT EXTEND macro are
+  deprecated. Use TYPED AS instead.
+
 ## Changes between Coq 8.8 and Coq 8.9
 
 ### ML API
-- 
cgit v1.2.3


From 41b640b46f9152c62271adaa930aa8e86a88f3e5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 14 Oct 2018 19:21:38 +0200
Subject: Documenting the transition from camlp5 to coqpp for ARGUMENT EXTEND.

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

(limited to 'dev/doc/changes.md')

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index c5632411d1..eb5b9ee1d3 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -214,7 +214,48 @@ END
 
 #### ARGUMENT EXTEND
 
-Not handled yet.
+Steps to perform:
+- replace the brackets enclosing OCaml code in actions with braces
+- if not there yet, add a leading `|` to the first rule
+- syntax of `TYPED AS` has been restricted not to accept compound generic
+  arguments as a literal, e.g. `foo_opt` should be rewritten into `foo option`
+  and similarly `foo_list` into `foo list`.
+- parenthesis around pair types in `TYPED AS` are now mandatory
+- `RAW_TYPED AS` and `GLOB_TYPED AS` clauses need to be removed
+
+`BY` clauses are considered OCaml code, and thus need to be wrapped in braces,
+but not the `TYPED AS` clauses.
+
+For instance, code of the form:
+```
+ARGUMENT EXTEND my_arg
+  TYPED AS int_opt
+  PRINTED BY printer
+  INTERPRETED BY interp_f
+  GLOBALIZED BY glob_f
+  SUBSTITUTED BY subst_f
+  RAW_TYPED AS int_opt
+  RAW_PRINTED BY raw_printer
+  GLOB_TYPED AS int_opt
+  GLOB_PRINTED BY glob_printer
+  [ "foo" int(i) ] -> [ my_arg1 i ]
+| [ "bar" ] -> [ my_arg2 ]
+END
+```
+should be turned into
+```
+ARGUMENT EXTEND my_arg
+  TYPED AS { int_opt }
+  PRINTED BY { printer }
+  INTERPRETED BY { interp_f }
+  GLOBALIZED BY { glob_f }
+  SUBSTITUTED BY { subst_f }
+  RAW_PRINTED BY { raw_printer }
+  GLOB_PRINTED BY { glob_printer }
+| [ "foo" int(i) ] -> { my_arg1 i }
+| [ "bar" ] -> { my_arg2 }
+END
+```
 
 #### GEXTEND
 
-- 
cgit v1.2.3