aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/ltac_match_pattern_names.v
blob: 790cd1b3a7331585b0b90a88261f751d3eb88d53 (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
(* example from bug 5345 *)
Ltac break_tuple :=
  match goal with
  | [ H: context[let '(n, m) := ?a in _] |- _ ] =>
    let n := fresh n in
    let m := fresh m in
    destruct a as [n m]
  end.

(* desugared version of break_tuple *)
Ltac break_tuple' :=
  match goal with
  | [ H: context[match ?a with | pair n m => _ end] |- _ ] =>
    let n := fresh n in
    let m := fresh m in
    idtac
  end.

Ltac multiple_branches :=
  match goal with
  | [ H: match _ with
         | left P => _
         | right Q => _
         end |- _ ] =>
    let P := fresh P in
    let Q := fresh Q in
    idtac
  end.