aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/PCase.v
blob: 67d680ba87327f2c9b6fc6dd4eaa9bc371b1c74f (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
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66

(** Some tests of patterns containing matchs ending with joker branches.
    Cf. the new form of the [constr_pattern] constructor [PCase]
    in [pretyping/pattern.ml] *)

(* A universal match matcher *)

Ltac kill_match :=
 match goal with
   |- context [ match ?x with _ => _ end ] => destruct x
 end.

(* A match matcher restricted to a given type : nat *)

Ltac kill_match_nat :=
 match goal with
   |- context [ match ?x in nat with _ => _ end ] => destruct x
 end.

(* Another way to restrict to a given type : give a branch *)

Ltac kill_match_nat2 :=
 match goal with
   |- context [ match ?x with S _ => _ | _ => _ end ] => destruct x
 end.

(* This should act only on empty match *)

Ltac kill_match_empty :=
 match goal with
   |- context [ match ?x with end ] => destruct x
 end.

Lemma test1 (b:bool) : if b then True else O=O.
Proof.
 Fail kill_match_nat.
 Fail kill_match_nat2.
 Fail kill_match_empty.
 kill_match. exact I. exact eq_refl.
Qed.

Lemma test2a (n:nat) : match n with O => True | S n => (n = n) end.
Proof.
 Fail kill_match_empty.
 kill_match_nat. exact I. exact eq_refl.
Qed.

Lemma test2b (n:nat) : match n with O => True | S n => (n = n) end.
Proof.
 kill_match_nat2. exact I. exact eq_refl.
Qed.

Lemma test2c (n:nat) : match n with O => True | S n => (n = n) end.
Proof.
 kill_match. exact I. exact eq_refl.
Qed.

Lemma test3a (f:False) : match f return Prop with end.
Proof.
 kill_match_empty.
Qed.

Lemma test3b (f:False) : match f return Prop with end.
Proof.
 kill_match.
Qed.