The Coq mailing list

[Dmitry Grebeniuk <gdsfh1 AT gmail.com>]

Hello.

> I believe [appcontext] only matches against genuine Gallina terms, not, say,
> sequences of arguments as in your example.  You could think of [appcontext]
> as matching _prefixes_ of applications, whereas your example tries to match
> a strict _suffix_.

  Thanks, you are right.  But is it the expected
behaviour of appcontext?

  So, I ended up with
    | |- appcontext [ (myid ?x) ] => ...
    | |- appcontext [ _ (myid ?x) ] => ...
    | |- appcontext [ _ _ (myid ?x) ] => ...
    [ 20 more lines skipped ]

  Looks beautiful, like stairs!