The Coq mailing list

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

Beta Ziliani wrote:
> If I don't recall wrong, this can be easily done with ssreflect. Of 
> course, you need to install that plugin, but that's a good idea anyway.

Thanks, that's good to know!  I would like to minimize the dependencies 
of the library I'm working on, so avoiding Ssreflect would be a plus.

> On Thu, Jan 5, 2012 at 7:45 PM, Adam Chlipala <adamc AT csail.mit.edu 
> <mailto:adamc AT csail.mit.edu>> wrote:
>
>     I'd like to write a tactic like this one:
>       Ltac evaluator ids := cbv beta zeta iota delta [plus minus ids].
>
>       ...evaluator foo bar baz...
>
>     In other words, the tactic acts like [compute], with the exception
>     that the only unfolded identifiers are [plus], [minus], and those
>     identifiers in the input identifier list [ids].  The real code
>     that inspired my question has many more identifiers that are
>     fixed, in addition to longer call-specific identifier lists.
>
>     The above doesn't do the job.  Is there a way in Ltac to do this
>     kind of abstraction over identifier lists?  (I can't find a way to
>     do it with [Tactic Notation], either.)
>
>     In case anyone is wondering why this sort of thing would be
>     useful: In the goals in question, [simpl] is too slow, and
>     [compute] unfolds identifiers that I don't want to disturb.  The
>     right instance of the above tactic schema finishes instantly and
>     produces pretty goals.