The Coq mailing list

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

Thanks, Robert. Works like a charm!

Sincerely,
Kirill Taran

On Wed, Jul 2, 2014 at 2:49 AM, Robbert Krebbers <mailinglists AT robbertkrebbers.nl> wrote:

Ltac matching is not up to delta, you should do something like

  match eval hnf in xs with
  ...
  end

You can change hnf to another evaluation strategy that may be more suitable for your case.

On 07/02/2014 12:43 AM, Kirill Taran wrote:

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