diff options
| author | coqbot-app[bot] | 2020-10-27 21:12:37 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-27 21:12:37 +0000 |
| commit | c8110e13cceab22dd855de7ee2114bcb4eedd699 (patch) | |
| tree | 9fa2c8f1922075942998828523137debf9bf0c1e /test-suite | |
| parent | 96354508a50f12a2af49bd95073c6a24cea69713 (diff) | |
| parent | 480d34fc22c195d4b19f639345fa993652838894 (diff) | |
Merge PR #13219: Rename mlg grammar nonterminals to make documented and mlg grammars more consistent
Reviewed-by: Zimmi48
Reviewed-by: herbelin
Ack-by: SkySkimmer
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/misc/quotation_token/src/quotation.mlg | 4 | ||||
| -rw-r--r-- | test-suite/output/Notations4.out | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/test-suite/misc/quotation_token/src/quotation.mlg b/test-suite/misc/quotation_token/src/quotation.mlg index 961b170a0d..ba0bcb1b3c 100644 --- a/test-suite/misc/quotation_token/src/quotation.mlg +++ b/test-suite/misc/quotation_token/src/quotation.mlg @@ -2,9 +2,9 @@ open Pcoq.Constr } GRAMMAR EXTEND Gram - GLOBAL: operconstr; + GLOBAL: term; - operconstr: LEVEL "0" + term: LEVEL "0" [ [ s = QUOTATION "foobar:" -> { CAst.make ~loc Constrexpr.(CSort Glob_term.(UNamed [GProp,0])) } ] ] diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index a42518822f..fa0c20bf73 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -8,7 +8,7 @@ Entry custom:myconstr is | "4" RIGHTA [ SELF; "*"; NEXT ] | "3" RIGHTA - [ "<"; operconstr LEVEL "10"; ">" ] ] + [ "<"; term LEVEL "10"; ">" ] ] [< b > + < b > * < 2 >] : nat @@ -77,7 +77,7 @@ The command has indeed failed with message: The format is not the same on the right- and left-hand sides of the special token "..". Entry custom:expr is [ "201" RIGHTA - [ "{"; operconstr LEVEL "200"; "}" ] ] + [ "{"; term LEVEL "200"; "}" ] ] fun x : nat => [ x ] : nat -> nat |