The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

Hi all,

I have a question regarding the extension of Ltac with ml code.

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.

Thanks,

—

Frédéric