diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /test-suite/output/Arguments_renaming.out | |
parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'test-suite/output/Arguments_renaming.out')
-rw-r--r-- | test-suite/output/Arguments_renaming.out | 22 |
1 files changed, 13 insertions, 9 deletions
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 1e3cc37d..b084ad49 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -1,13 +1,17 @@ The command has indeed failed with message: Error: To rename arguments the "rename" flag must be specified. Argument A renamed to B. -The command has indeed failed with message: -Error: To rename arguments the "rename" flag must be specified. -Argument A renamed to T. +File "stdin", line 2, characters 0-25: +Warning: This command is just asserting the names of arguments of identity. +If this is what you want add ': assert' to silence the warning. If you want +to clear implicit arguments add ': clear implicits'. If you want to clear +notation scopes add ': clear scopes' [arguments-assert,vernacular] @eq_refl : forall (B : Type) (y : B), y = y -@eq_refl nat - : forall x : nat, x = x +eq_refl + : ?y = ?y +where +?y : [ |- nat] Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x For eq_refl: Arguments are renamed to B, y @@ -99,15 +103,15 @@ Expands to: Constant Top.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. +Error: Argument lists should agree on the names they provide. The command has indeed failed with message: -Error: The following arguments are not declared: x. +Error: Sequences of implicit arguments must be of different lengths. The command has indeed failed with message: -Error: Arguments names must be distinct. +Error: Some argument names are duplicated: F The command has indeed failed with message: Error: Argument z cannot be declared implicit. The command has indeed failed with message: -Error: Extra argument y. +Error: Extra arguments: y. The command has indeed failed with message: Error: To rename arguments the "rename" flag must be specified. Argument A renamed to R. |