The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 07/27/2016 04:00 PM, Clément Pit--Claudel wrote:
> On 2016-07-27 15:06, Robbert Krebbers wrote:
> > On 07/27/2016 09:04 PM, Jonathan Leivent wrote:
> > > On 07/27/2016 02:59 PM, Matthieu Sozeau wrote:
> > > > .. Maybe a
> > > > modifier like unshelve would be more suited.
> > > +1
> > And my +2!
> Are we slowly rediscovering dynamically scoped variables? :) In Lisp, one 
> would write something like this:
>
> (let ((unshelve t)
>        (tc-resolution nil))
>    (apply <some-theorem>))
>
> And the implementation of 'apply' would obey 'unshelve' and 'tc-resolution' 
> (and probably many other settings, such as whether to print debugging 
> information).  Maybe a unified mechanism like this would be nice to have in 
> ltac 2.0? It would allow tactic writers to make their own tactics 
> customizable, without resorting to opacity-based tricks.
>
> Cheers,
> Clément.

+1

I recommended something like this to Hugo in a comment on a pr 
recently.  Even for things like various Set/Unset commands.

-- Jonathan