diff options
| author | coqbot-app[bot] | 2020-11-23 15:06:48 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-23 15:06:48 +0000 |
| commit | 5fce39e0078935662fd6fb9b8e2ee6b0da60b3ab (patch) | |
| tree | efc105da1f224ef87400e4bab4779670b8057827 /doc/tools/docgram/orderedGrammar | |
| parent | 94d579844817edcbb2454dd9dc79071b2cd1d12a (diff) | |
| parent | 87c46c50506089ba16bdd7afd7e795ee21033319 (diff) | |
Merge PR #11841: Distinguishing entry "ident" from entry "name" in term notations.
Reviewed-by: jfehrle
Reviewed-by: gares
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
Diffstat (limited to 'doc/tools/docgram/orderedGrammar')
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index c27169d432..f62dd8f731 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -1579,6 +1579,7 @@ syntax_modifier: [ explicit_subentry: [ | "ident" +| "name" | "global" | "bigint" | "strict" "pattern" OPT ( "at" "level" natural ) @@ -1591,6 +1592,7 @@ explicit_subentry: [ binder_interp: [ | "as" "ident" +| "as" "name" | "as" "pattern" | "as" "strict" "pattern" ] |