The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 20/09/2016 12:09, Frédéric Besson wrote:
> I know that you can extend Ltac with a ml tactic. I am wondering
> whether someone knows how to extend the *functional *language of Ltac
> with a ml function. For instance, the ml function would perform some
> computation over an argument Coq term and return another Coq term.

It's not possible currently, because of the limitations of Ltac
semantics (namely, the TacML node is evaluated by-value). I think we
could hack around that by defining a generic argument whose
interpretation function would precisely be the ML function you want to
use, but this is reaaaaaally ugly. If you've got an urgent usecase, you
can probably tell it on this list so we can help you.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature