diff options
| author | coqbot-app[bot] | 2020-10-04 20:01:35 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-04 20:01:35 +0000 |
| commit | 6d3a9220204de22e0b81dc961d2eb269128b5c2e (patch) | |
| tree | 44d20f3ea71f1c65b85c564c5f3d376dc8e57191 /test-suite | |
| parent | e596bbb66b8a0ea6fe396315972f7743f8258a97 (diff) | |
| parent | 5b194f6c4f16b99fe8ebe3c8004c31c01aec0b3b (diff) | |
Merge PR #13096: Drop prefixes from non-terminal names, e.g. "constr:constr" -> "constr"
Reviewed-by: herbelin
Ack-by: Zimmi48
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations4.out | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index ce51acac95..a42518822f 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -1,6 +1,6 @@ [< 0 > + < 1 > * < 2 >] : nat -Entry constr:myconstr is +Entry custom:myconstr is [ "6" RIGHTA [ ] | "5" RIGHTA @@ -8,7 +8,7 @@ Entry constr:myconstr is | "4" RIGHTA [ SELF; "*"; NEXT ] | "3" RIGHTA - [ "<"; constr:operconstr LEVEL "10"; ">" ] ] + [ "<"; operconstr LEVEL "10"; ">" ] ] [< b > + < b > * < 2 >] : nat @@ -75,9 +75,9 @@ The command has indeed failed with message: The format is not the same on the right- and left-hand sides of the special token "..". 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 constr:expr is +Entry custom:expr is [ "201" RIGHTA - [ "{"; constr:operconstr LEVEL "200"; "}" ] ] + [ "{"; operconstr LEVEL "200"; "}" ] ] fun x : nat => [ x ] : nat -> nat |