diff options
| author | Maxime Dénès | 2018-10-11 12:30:50 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-10-11 12:30:50 +0200 |
| commit | 4a244648cff78c7f7333ac5b335de3f6e742908a (patch) | |
| tree | 717b267cc2e2ae1359bfcb2bb7f30b2f5bde9640 /dev | |
| parent | 2bdc3a06c5620bf4796501562886b26f8c1ef895 (diff) | |
| parent | bc240341d9f0f7466c82e8ee9f3f325cda6fc3bf (diff) | |
Merge PR #8161: Implement VERNAC EXTEND in coqpp
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 |