diff options
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index dbc1b4a21b..c29f564945 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -103,7 +103,7 @@ The reduction tactics unfold myplus when the 2nd and 3rd arguments evaluate to a constructor myplus is transparent Expands to: Constant Top.myplus -myplus +@myplus : forall Z : Type, Z -> nat -> nat -> nat The command has indeed failed with message: => Error: All arguments lists must declare the same names. |