diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-12 11:33:08 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-12 13:37:14 +0200 |
| commit | c7480636bce632adfa28d6bb0b423a086ade4318 (patch) | |
| tree | 24fbca8dbed1d873064ce2a2473947a6d10e17d6 /test-suite/output/Arguments_renaming.out | |
| parent | c0316d627b80b1e81fc020762f835a1695966a64 (diff) | |
Upgrading output tests.
output/Arguments.v
output/ArgumentsScope.v
output/Arguments_renaming.v
output/Cases.v
output/Implicit.v
output/PrintInfos.v
output/TranspModType.v
Main changes: monomorphic -> not universe polymorphic, Peano vs Nat
Diffstat (limited to 'test-suite/output/Arguments_renaming.out')
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index c440d5ba7..c99dfc018 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -20,7 +20,7 @@ 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 monomorphic +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 +36,7 @@ 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 monomorphic +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 +49,13 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -myplus is monomorphic +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 monomorphic +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 +74,7 @@ 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 monomorphic +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 +89,13 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -myplus is monomorphic +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 monomorphic +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] |