diff options
| author | coqbot-app[bot] | 2020-11-20 09:21:27 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-20 09:21:27 +0000 |
| commit | 122aef582e69f692e6720097a3fac7e0d4d41bcd (patch) | |
| tree | 062a2e1a02e687d5f5fe68b6dd949ee2b4c9dbae /doc/tools/docgram/common.edit_mlg | |
| parent | 57c85b0d54e54ca33238399cab3285ef34d4edd2 (diff) | |
| parent | 00003b625ed3d5f3f2d79cf38ca6ad08e634432e (diff) | |
Merge PR #13403: Use only nats for occs_nums rather than ints
Reviewed-by: Zimmi48
Reviewed-by: herbelin
Diffstat (limited to 'doc/tools/docgram/common.edit_mlg')
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 4c1956d172..816acba4c1 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1939,11 +1939,6 @@ tac2rec_fields: [ | LIST1 tac2rec_field SEP ";" OPT ";" TAG Ltac2 ] -(* todo: weird productions, ints only after an initial "-"??: - occs_nums: [ - | LIST1 [ natural | ident ] - | "-" [ natural | ident ] LIST0 int_or_var -*) ltac2_occs_nums: [ | DELETE LIST1 nat_or_anti (* Ltac2 plugin *) | REPLACE "-" nat_or_anti LIST0 nat_or_anti (* Ltac2 plugin *) |