diff options
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 3 | ||||
| -rw-r--r-- | test-suite/output/PrintInfos.v | 2 |
2 files changed, 3 insertions, 2 deletions
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index ba4bc070c6..3f0717666c 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -113,7 +113,8 @@ Sequences of implicit arguments must be of different lengths. The command has indeed failed with message: Some argument names are duplicated: F The command has indeed failed with message: -Argument z cannot be declared implicit. +Argument number 2 (anonymous in original definition) cannot be declared +implicit. The command has indeed failed with message: Extra arguments: y. The command has indeed failed with message: diff --git a/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v index d7c271c3ec..d95cc0e32f 100644 --- a/test-suite/output/PrintInfos.v +++ b/test-suite/output/PrintInfos.v @@ -22,7 +22,7 @@ Print comparison. Definition foo := forall x, x = 0. Parameter bar : foo. -Arguments bar [x]. +Arguments bar {x}. About bar. Print bar. |