diff options
Diffstat (limited to 'test-suite/output/Arguments_renaming.out')
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 23 |
1 files changed, 8 insertions, 15 deletions
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index c29f5649..1e3cc37d 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -1,8 +1,8 @@ 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. 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 T. @eq_refl : forall (B : Type) (y : B), y = y @@ -20,7 +20,6 @@ For eq: Argument scopes are [type_scope _ _] For eq_refl: Argument scopes are [type_scope _] eq_refl : forall (A : Type) (x : A), x = x -eq_refl is not universe polymorphic Arguments are renamed to B, y When applied to no arguments: Arguments B, y are implicit and maximally inserted @@ -36,7 +35,6 @@ For myEq: Argument scopes are [type_scope _ _] For myrefl: Argument scopes are [type_scope _ _] myrefl : forall (B : Type) (x : A), B -> myEq B x x -myrefl is not universe polymorphic Arguments are renamed to C, x, _ Argument C is implicit and maximally inserted Argument scopes are [type_scope _ _] @@ -49,13 +47,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -myplus is not universe polymorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] myplus : forall T : Type, T -> nat -> nat -> nat -myplus is not universe polymorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] @@ -74,7 +70,6 @@ For myEq: Argument scopes are [type_scope type_scope _ _] For myrefl: Argument scopes are [type_scope type_scope _ _] myrefl : forall (A B : Type) (x : A), B -> myEq A B x x -myrefl is not universe polymorphic Arguments are renamed to A, C, x, _ Argument C is implicit and maximally inserted Argument scopes are [type_scope type_scope _ _] @@ -89,13 +84,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -myplus is not universe polymorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] myplus : forall T : Type, T -> nat -> nat -> nat -myplus is not universe polymorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] @@ -106,15 +99,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: All arguments lists must declare the same names. The command has indeed failed with message: -=> Error: The following arguments are not declared: x. +Error: The following arguments are not declared: x. The command has indeed failed with message: -=> Error: Arguments names must be distinct. +Error: Arguments names must be distinct. The command has indeed failed with message: -=> Error: Argument z cannot be declared implicit. +Error: Argument z cannot be declared implicit. The command has indeed failed with message: -=> Error: Extra argument y. +Error: Extra argument y. 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. |