blob: 785844c66d1311e778f24c2ef7a993ca6f67da27 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
(* Destruct and primitive projections *)
(* Checking the (superficial) part of #5707:
"destruct" should be able to use non-dependent case analysis when
dependent case analysis is not available and unneeded *)
Set Primitive Projections.
Inductive foo := Foo { proj1 : nat; proj2 : nat }.
Goal forall x : foo, True.
Proof. intros x. destruct x.
|
