aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/1865.v
blob: 17c19989488b7f649b19062e9f2e841017d08db7 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
(* Check that tactics (here dependent inversion) do not generate
   conversion problems T <= U with sup's of universes in U *)

(* Submitted by David Nowak *)

Inductive list (A:Set) : nat -> Set :=
| nil : list A O
| cons : forall n, A -> list A n -> list A (S n).

Definition f (n:nat) : Type :=
  match n with
  | O => bool
  | _ => unit
  end.

Goal forall A n, list A n -> f n.
intros A n.
dependent inversion n.