blob: eb37141bcfb8110fd2659758116183339bdc4aa7 (
plain)
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
37
|
(* Check that the subterms of the predicate of a match are taken into account *)
Require Import List.
Open Scope list_scope.
Goal forall A (x x' : A) (xs xs' : list A) (H : x::xs = x'::xs'),
let k :=
(match H in (_ = y) return x = hd x y with
| eq_refl => eq_refl
end : x = x')
in k = k.
simpl.
intros.
match goal with
| [ |- context G[@hd] ] => idtac
end.
(* This second example comes from CFGV where inspecting subterms of a
match is expecting to inspect first the term to match (even though
it would certainly be better to provide a "match x with _ end"
construct for generically matching a "match") *)
Ltac find_head_of_head_match T :=
match T with context [?E] =>
match T with
| E => fail 1
| _ => constr:(E)
end
end.
Ltac mydestruct :=
match goal with
| |- ?T1 = _ => let E := find_head_of_head_match T1 in destruct E
end.
Goal forall x, match x with 0 => 0 | _ => 0 end = 0.
intros.
mydestruct.
|
