The Coq mailing list

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

Hello --

Is there any support for Ltac matching of [fix] expressions? For example, if I have a goal like:

Goal 1 + 1 = 2.

  cbv delta [ plus ].

  match goal with

    | [ |- ? 1 1 = 2 ] =>

  end.

Is there anything that I could fill in that question mark with besides a ?variable or _ that would match the goal? If not, this seems like it is missing and would be very useful, even if it was just viewed exactly the same way as [fun _ => _].

Thanks.

--
gregory malecha

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