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
34
35
36
|
Set Primitive Projections.
Record Box (A:Type) := box { unbox : A }.
Definition ubox := @unbox.
Axiom trip : nat -> nat -> nat -> Prop.
Ltac show_goal := match goal with |- ?g => idtac g end.
Lemma foo (n:Box nat) :
(* constant, folded, unfolded *)
trip (ubox _ n) (unbox _ n) (match n with box _ n => n end).
Proof.
simpl. (* remove extra letins introduced by match compilation *)
cbv delta [ubox].
show_goal.
Set Printing Unfolded Projection As Match.
show_goal.
Set Printing Projections.
show_goal.
Unset Printing Unfolded Projection As Match.
show_goal.
Arguments unbox {_}.
show_goal.
Set Printing Unfolded Projection As Match.
show_goal.
Unset Printing Projections.
show_goal.
Abort.
|
