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?
The current problem is
no implementation available for Tac2ffi on
Declare ML Module "my_plugin".
missing open Ltac2_plugin?
I think that is correct! Thanks!
Last updated: Oct 16 2021 at 03:02 UTC