The Coq mailing list

[Gregory Malecha <gmalecha AT eecs.harvard.edu>]

Hello --

I am wondering what the semantics of Ltac should be with respect to constructing open terms. I feel like when I started using Coq Ltac was only supposed to be able to generate closed terms, but I've been trying some things out on 8.4b2 and it seems like that may have changed. Here's what I wrote:

Goal (fun x => 0) = (fun x => x).

  match goal with

   | [ |- ?L = ?R ] =>

     match R with

       | (fun x => ?R) => idtac R

     end

  end.

This prints "x", I was under the impression that it would fail. This, on the other hand, will fail.

Goal (fun x => 0) = (fun x => x).

  match goal with

   | [ |- ?L = ?R ] =>

     match R with

       | (fun x => ?R) => idtac R

     end

  end.

Is this the desired behavior? It doesn't seem like [x] is a binder here. I'm wondering if I should report this as a bug.

Thanks.

--
gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/