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/Cases.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/Cases.out')
| -rw-r--r-- | test-suite/output/Cases.out | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 152a722aa..c768f09ce 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -7,7 +7,7 @@ fix F (t : t) : P t := : forall P : t -> Type, (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t -t_rect is monomorphic +t_rect is not universe polymorphic proj = fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) => match Nat.eq_dec x y with @@ -18,7 +18,7 @@ match Nat.eq_dec x y with end : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y -proj is monomorphic +proj is not universe polymorphic Argument scopes are [nat_scope nat_scope _ _ _] foo = fix foo (A : Type) (l : list A) {struct l} : option A := @@ -29,7 +29,7 @@ fix foo (A : Type) (l : list A) {struct l} : option A := end : forall A : Type, list A -> option A -foo is monomorphic +foo is not universe polymorphic Argument scopes are [type_scope list_scope] uncast = fun (A : Type) (x : I A) => match x with @@ -37,12 +37,12 @@ fun (A : Type) (x : I A) => match x with end : forall A : Type, I A -> A -uncast is monomorphic +uncast is not universe polymorphic Argument scopes are [type_scope _] foo' = if A 0 then true else false : bool -foo' is monomorphic +foo' is not universe polymorphic f = fun H : B => match H with @@ -54,4 +54,4 @@ match H with end : B -> True -f is monomorphic +f is not universe polymorphic |