Stream: Coq devs & plugin devs

Topic: Extending Ltac2

view this post on Zulip Janno (Oct 30 2020 at 15:07):

I am trying to provide a new ltac2 primitive(?) with a plugin and I am running into different OCaml/plugin related issues because I do not know what I am doing. Is there perhaps an example of how to add ltac2 primitives in a plugin?

view this post on Zulip Janno (Oct 30 2020 at 15:13):

The current problem is no implementation available for Tac2ffi on Declare ML Module "my_plugin".

view this post on Zulip Gaëtan Gilbert (Oct 30 2020 at 15:27):

missing open Ltac2_plugin?

view this post on Zulip Janno (Oct 30 2020 at 15:44):

I think that is correct! Thanks!

Last updated: Apr 18 2024 at 19:02 UTC