diff options
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/Notations4.out | 4 |
1 files changed, 2 insertions, 2 deletions
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 |