diff options
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 6 | ||||
| -rw-r--r-- | test-suite/output/ltac.out | 3 |
2 files changed, 6 insertions, 3 deletions
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 1633ad976..e665db47d 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -2,7 +2,8 @@ File "stdin", line 1, characters 0-36: Warning: Ignoring rename of x into y. Only implicit arguments can be renamed. [arguments-ignore-rename-nonimpl,vernacular] The command has indeed failed with message: -Error: To rename arguments the "rename" flag must be specified. +Error: +To rename arguments the "rename" flag must be specified. Argument A renamed to B. File "stdin", line 2, characters 0-25: Warning: Ignoring rename of A into T. Only implicit arguments can be renamed. @@ -125,5 +126,6 @@ File "stdin", line 53, characters 0-26: Warning: Ignoring rename of x into s. Only implicit arguments can be renamed. [arguments-ignore-rename-nonimpl,vernacular] The command has indeed failed with message: -Error: To rename arguments the "rename" flag must be specified. +Error: +To rename arguments the "rename" flag must be specified. Argument A renamed to R. diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index f4254e4e2..a2d545202 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -1,5 +1,6 @@ The command has indeed failed with message: -Error: Ltac variable y depends on pattern variable name z which is not bound in current context. +Error: +Ltac variable y depends on pattern variable name z which is not bound in current context. Ltac f x y z := symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize dependent z |