coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] matching a function application?

From: Tom Prince <tom.prince AT ualberta.net>
To: Chung-Kil Hur <gil.hur AT gmail.com>, Coq Club <coq-club AT inria.fr>
Cc: Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>
Subject: Re: [Coq-Club] matching a function application?
Date: Sun, 04 Dec 2011 16:23:08 -0500

On Mon, 28 Nov 2011 21:02:40 +0100, Chung-Kil Hur
<gil.hur AT gmail.com>
wrote:
> As far as I know, "context" exists for backward compatibility.
> - Gil

Would it be reasonable to have an option to turn context into
appcontext? I would guess that the only reason not to have that always
is for backwards compatility, so new developments would benefit by
having the app context as the default behavior.

Tom

Re: [Coq-Club] matching a function application?, Tom Prince