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/PrintInfos.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/PrintInfos.out')
| -rw-r--r-- | test-suite/output/PrintInfos.out | 32 |
1 files changed, 16 insertions, 16 deletions
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index 62889f802..2b010f067 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -25,7 +25,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 When applied to no arguments: Arguments A, x are implicit and maximally inserted When applied to 1 argument: @@ -38,27 +38,27 @@ When applied to no arguments: Arguments A, x are implicit and maximally inserted When applied to 1 argument: Argument A is implicit -plus = -fix plus (n m : nat) {struct n} : nat := +Nat.add = +fix add (n m : nat) {struct n} : nat := match n with | 0 => m - | S p => S (plus p m) + | S p => S (add p m) end : nat -> nat -> nat -plus is monomorphic +Nat.add is not universe polymorphic Argument scopes are [nat_scope nat_scope] -plus : nat -> nat -> nat +Nat.add : nat -> nat -> nat -plus is monomorphic +Nat.add is not universe polymorphic Argument scopes are [nat_scope nat_scope] -plus is transparent -Expands to: Constant Coq.Init.Peano.plus -plus : nat -> nat -> nat +Nat.add is transparent +Expands to: Constant Coq.Init.Nat.add +Nat.add : nat -> nat -> nat plus_n_O : forall n : nat, n = n + 0 -plus_n_O is monomorphic +plus_n_O is not universe polymorphic Argument scope is [nat_scope] plus_n_O is opaque Expands to: Constant Coq.Init.Peano.plus_n_O @@ -80,13 +80,13 @@ For le_n: Argument scope is [nat_scope] For le_S: Argument scopes are [nat_scope nat_scope _] comparison : Set -comparison is monomorphic +comparison is not universe polymorphic Expands to: Inductive Coq.Init.Datatypes.comparison Inductive comparison : Set := Eq : comparison | Lt : comparison | Gt : comparison bar : foo -bar is monomorphic +bar is not universe polymorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 @@ -94,14 +94,14 @@ Argument x is implicit and maximally inserted Expands to: Constant Top.bar *** [ bar : foo ] -bar is monomorphic +bar is not universe polymorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 Argument x is implicit and maximally inserted bar : foo -bar is monomorphic +bar is not universe polymorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 @@ -109,7 +109,7 @@ Argument x is implicit and maximally inserted Expands to: Constant Top.bar *** [ bar : foo ] -bar is monomorphic +bar is not universe polymorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 |