diff options
| author | Hugo Herbelin | 2020-07-14 18:23:31 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-22 13:28:40 +0100 |
| commit | 87c46c50506089ba16bdd7afd7e795ee21033319 (patch) | |
| tree | 83097b8fb1664f404296e4b4c09ebefe620bd50a /doc/tools | |
| parent | df8b5c7d83ad6e88af34d29bcc32c85bd42c2712 (diff) | |
Updating doc wrt addition of grammar subentry "name" and deprecation of "ident".
For constr, this means clarifying that "ident" is deprecated and to be
replaced by "name". Here, some cleaning shall have to be done at the
end of deprecation phase, when "ident" will take its literal meaning.
For custom notations, this is about documenting the effect of "ident"
and "global" which was yet undocumented.
Note that we anticipate an example in constr working with the literal
meaning of "ident" (temporarily silencing the warning).
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
Diffstat (limited to 'doc/tools')
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 2 | ||||
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 2 |
2 files changed, 4 insertions, 0 deletions
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 03a20d621b..e23925d1f7 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1420,6 +1420,7 @@ syntax_modifiers: [ explicit_subentry: [ | "ident" +| "name" | "global" | "bigint" | "binder" @@ -1440,6 +1441,7 @@ at_level_opt: [ binder_interp: [ | "as" "ident" +| "as" "name" | "as" "pattern" | "as" "strict" "pattern" ] diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 0209cf762a..1948d48dbd 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -1574,6 +1574,7 @@ syntax_modifier: [ explicit_subentry: [ | "ident" +| "name" | "global" | "bigint" | "strict" "pattern" OPT ( "at" "level" natural ) @@ -1586,6 +1587,7 @@ explicit_subentry: [ binder_interp: [ | "as" "ident" +| "as" "name" | "as" "pattern" | "as" "strict" "pattern" ] |