aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/univers.v
blob: 269359ae62f3fa3c5354f044d003389209678f95 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
(* This requires cumulativity *)

Definition Type2 := Type.
Definition Type1 : Type2 := Type.

Lemma lem1 : (True -> Type1) -> Type2.
intro H.
apply H.
exact I.
Qed.

Lemma lem2 :
 forall (A : Type) (P : A -> Type) (x : A),
 (forall y : A, x = y -> P y) -> P x.
auto.
Qed.

Lemma lem3 : forall P : Prop, P.
intro P; pattern P.
apply lem2.
Abort.

(* Check managing of universe constraints in inversion *)
(* Bug report #855 *)

Inductive dep_eq : forall X : Type, X -> X -> Prop :=
  | intro_eq : forall (X : Type) (f : X), dep_eq X f f
  | intro_feq :
      forall (A : Type) (B : A -> Type),
      let T := forall x : A, B x in
      forall (f g : T) (x : A), dep_eq (B x) (f x) (g x) -> dep_eq T f g.

Require Import Relations.

Theorem dep_eq_trans : forall X : Type, transitive X (dep_eq X).
Proof.
  unfold transitive.
  intros X f g h H1 H2.
  inversion H1.
Abort.


(* Submitted by Bas Spitters (bug report #935) *)

(* This is a problem with the status of the type in LetIn: is it a
   user-provided one or an inferred one? At the current time, the
   kernel type-check the type in LetIn, which means that it must be
   considered as user-provided when calling the kernel. However, in
   practice it is inferred so that a universe refresh is needed to set
   its status as "user-provided".

   Especially, universe refreshing was not done for "set/pose" *)

Lemma ind_unsec : forall Q : nat -> Type, True.
intro.
set (C := forall m, Q m -> Q m).
exact I.
Qed.

(* Submitted by Danko Ilik (bug report #1507); related to LetIn *)

Record U : Type := { A:=Type; a:A }.

(** Check assignement of sorts to inductives and records. *)

Variable sh : list nat.

Definition is_box_in_shape (b :nat * nat) := True.
Definition myType := Type.

Module Ind.
Inductive box_in : myType :=
  myBox (coord : nat * nat) (_ : is_box_in_shape coord) : box_in.
End Ind.

Module Rec.
Record box_in : myType :=
  BoxIn { coord :> nat * nat; _ : is_box_in_shape coord }.
End Rec.