The Coq mailing list

[Dmitry Grebeniuk <gdsfh1 AT gmail.com>]

Hello.

  Documentation says about "match goal with ... appcontext":

"
The behavior of appcontext is the same as the one of context,
except that a matching subterm could be a partial part of a
longer application.
"

  I don't understand is it a bug or not (so I'm writing here and
I'm not filing a bug), but in my case "appcontext" doesn't
work as I expect it to work:


Require Import Arith.
Goal (plus 1 (id 2)) = 3.
match goal with
| |- appcontext [ _ (id _) ] => idtac "found"
end.
(* Error: No matching clauses for match goal *)

  "context [ _ _ (id _) ]" matches the goal, and I thought
that "appcontext" could be used exactly in these
situations, since "plus 1 (id 2)" can be seen as partial
application: "(plus 1) (id 2)", so it could be matched
by "[ _ (id _) ]".
  It seems that I don't understand "appcontext", right?