The Coq mailing list

[Chung-Kil Hur <gil.hur AT gmail.com>]

As far as I know, "context" exists for backward compatibility.
- Gil

On Mon, Nov 28, 2011 at 7:46 PM, Michael Shulman 
<mshulman AT ucsd.edu>
 wrote:
> On Mon, Nov 28, 2011 at 4:15 PM, Chung-Kil Hur 
>Â <gil.hur AT gmail.com>
>  wrote:
>> Use appcontext.
>
> Awesome, thank you!
>
> On Mon, Nov 28, 2011 at 07:25, Alexandre Pilkiewicz
>Â <alexandre.pilkiewicz AT polytechnique.org>
>  wrote:
>> That might be a great thing to add to the documentation :)
>
> Hear, hear!
>
> What exactly is the difference between appcontext and context?  In
> what situations would one want to use context rather than appcontext?
> (I presume there are some, otherwise why not just add this
> functionality to context instead of creating appcontext?)
>
> Mike
>