aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/Cases.out
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-03-09 08:26:00 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-03-09 08:26:00 +0100
commite4ad47fed594d6865f5bd29a159976cb072f0fae (patch)
tree893bd81fe7df422d7c0a2bd545650a1e7ca86268 /test-suite/output/Cases.out
parentd337afac6f9b1fe405c89b4e62f660cadf171f0f (diff)
Do not display the status of monomorphic constants unless in universe-polymorphism mode.
Diffstat (limited to 'test-suite/output/Cases.out')
-rw-r--r--test-suite/output/Cases.out9
1 files changed, 0 insertions, 9 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index d59034836..09f032d47 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -6,8 +6,6 @@ fix F (t : t) : P t :=
end
: forall P : t -> Type,
(let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
-
-t_rect is not universe polymorphic
= fun d : TT => match d with
| @CTT _ _ b => b
end
@@ -26,7 +24,6 @@ match Nat.eq_dec x y with
end
: forall (x y : nat) (P : nat -> Type), P x -> P y -> P y
-proj is not universe polymorphic
Argument scopes are [nat_scope nat_scope _ _ _]
foo =
fix foo (A : Type) (l : list A) {struct l} : option A :=
@@ -37,7 +34,6 @@ fix foo (A : Type) (l : list A) {struct l} : option A :=
end
: forall A : Type, list A -> option A
-foo is not universe polymorphic
Argument scopes are [type_scope list_scope]
uncast =
fun (A : Type) (x : I A) => match x with
@@ -45,12 +41,9 @@ fun (A : Type) (x : I A) => match x with
end
: forall A : Type, I A -> A
-uncast is not universe polymorphic
Argument scopes are [type_scope _]
foo' = if A 0 then true else false
: bool
-
-foo' is not universe polymorphic
f =
fun H : B =>
match H with
@@ -61,5 +54,3 @@ match H with
else fun _ : P false => Logic.I) x
end
: B -> True
-
-f is not universe polymorphic