aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3210.v
blob: bb673f38c236372ea2e090782edfe17148267d4a (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
(* Test support of let-in in arity of inductive types *)

Inductive Foo : let X := Set in X :=
| I : Foo.

Definition foo (x : Foo) : bool :=
  match x with
  I => true
  end.

Definition foo' (x : Foo) : x = x.
case x.
match goal with |- I = I => idtac end. (* check form of the goal *)
Undo 2.
elim x.
match goal with |- I = I => idtac end. (* check form of the goal *)
Undo 2.
induction x.
match goal with |- I = I => idtac end. (* check form of the goal *)
Undo 2.
destruct x.
match goal with |- I = I => idtac end. (* check form of the goal *)