From 87c46c50506089ba16bdd7afd7e795ee21033319 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 14 Jul 2020 18:23:31 +0200 Subject: 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 Co-authored-by: Jim Fehrle --- doc/tools/docgram/fullGrammar | 2 ++ doc/tools/docgram/orderedGrammar | 2 ++ 2 files changed, 4 insertions(+) (limited to 'doc/tools/docgram') 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" ] -- cgit v1.2.3