diff options
| author | Pierre-Marie Pédrot | 2018-09-13 15:54:08 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-02 09:27:47 +0200 |
| commit | bc240341d9f0f7466c82e8ee9f3f325cda6fc3bf (patch) | |
| tree | 458d01bb58cbced90ce769eeb5a6eab15cbf6c3f /dev | |
| parent | 1407a1caabd5891552043e9f62e5f2058df07034 (diff) | |
Make the coqpp VERNAC EXTEND behave as the non-FUNCTIONAL camlp5 one.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/changes.md | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 157f41bd7b..0e35583b14 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -167,11 +167,6 @@ Steps to perform: 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 @@ -182,8 +177,8 @@ 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 } +| [ "foo" int(i) ] => { classif' } -> { cmd1 i } +| [ "bar" ] -> { cmd2 } END ``` |