The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

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.

Attachment: signature.asc
Description: OpenPGP digital signature