diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/changes.md | 48 |
1 files changed, 47 insertions, 1 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md index f30b4107b6..eb5b9ee1d3 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 @@ -209,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 |