blob: 096069049ae0bcf5d37edb94e510ecfbe18dd017 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
(* 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.
Abort.
|
