The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

Hello,

I am implementing a tricky tactic with match on "regular" values.
Match works ok for inlined values, but fails on values binded to a variable.

Here is minimized example:

Ltac matching xs tac :=
  match xs with
  | cons ?X ?XS => idtac "cons"
  | nil         => idtac "nil"
  end.

Goal 2 + 1 = 3.
  (* works:   *)
  matching (cons 1 (cons 2 (@nil nat))) show.

  (* doesn't: *)
  Definition l : list nat :=
    cons 1 (cons 2 (cons 3 (@nil nat))).
  matching l show.
Qed.

Error is "No matching clauses for match".

Sincerely,
Kirill Taran