aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3807.v
blob: 108ebf592bc431b04b0709f6c387f1e2354abe99 (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
Set Universe Polymorphism.
Set Printing Universes.
Unset Universe Minimization ToSet.


Definition foo : Type := nat.
About foo.
(* foo@{Top.1} : Type@{Top.1}*)
(* Top.1 |=  *)

Definition bar : foo -> nat.
Admitted.
About bar.
(* bar@{Top.2} : foo@{Top.2} -> nat *)
(* Top.2 |=  *)

Lemma baz@{i} : foo@{i} -> nat.
Proof.
  exact bar.
Defined.

Definition bar'@{i} : foo@{i} -> nat.
  intros f. exact 0.
Admitted.
About bar'.
(* bar'@{i} : foo@{i} -> nat *)
(* i |=  *)

Axiom f@{i} : Type@{i}.
(*
*** [ f@{i} : Type@{i} ]
(* i |=  *)
*)