The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 03/13/2013 08:30 AM, Dmitry Grebeniuk wrote:
> > 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?
>    

It's certainly what _I_ was expecting. :-)  I don't think it's a bug.