aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/abstract_poly.v
blob: aa8da53361e322e13920b73931d386bc7247d95d (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
Set Universe Polymorphism.

Inductive path@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := refl : path x x.
Inductive unit@{i} : Type@{i} := tt.

Lemma foo@{i j} : forall (m n : unit@{i}) (P : unit -> Type@{j}), path m n -> P m -> P n.
Proof.
intros m n P e p.
abstract (rewrite e in p; exact p).
Defined.

Check foo_subproof@{Set Set}.

Lemma bar : forall (m n : unit) (P : unit -> Type), path m n -> P m -> P n.
Proof.
intros m n P e p.
abstract (rewrite e in p; exact p).
Defined.

Check bar_subproof@{Set Set}.