summaryrefslogtreecommitdiff
path: root/test-suite/success/univers.v
blob: 87edc4debe2ca74d2a0287853e34225f86879bfe (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
(* 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 in |- *.
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 in |- *.
  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.