diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/changes.md | 23 | ||||
| -rw-r--r-- | dev/top_printers.ml | 4 |
2 files changed, 24 insertions, 3 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 7e64f80ac5..40013712fd 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -176,7 +176,28 @@ 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. + +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' } -> { cmd1 i } +| [ "bar" ] -> { cmd2 } +END +``` #### ARGUMENT EXTEND diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 8129a4a867..44d44ccc4b 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -527,7 +527,7 @@ let _ = extend_vernac_command_grammar ("PrintConstr", 0) None [GramTerminal "PrintConstr"; GramNonTerminal - (Loc.tag (Some (rawwit wit_constr),Extend.Aentry Pcoq.Constr.constr))] + (Loc.tag (rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr))] let _ = try @@ -543,7 +543,7 @@ let _ = extend_vernac_command_grammar ("PrintPureConstr", 0) None [GramTerminal "PrintPureConstr"; GramNonTerminal - (Loc.tag (Some (rawwit wit_constr),Extend.Aentry Pcoq.Constr.constr))] + (Loc.tag (rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr))] (* Setting printer of unbound global reference *) open Names |