Is there any better way to run Ltac2 from OCaml than to hand-build some AST and call
what does running ltac2 from ocaml mean if you don't have an ast?
I don't have the AST, but I think my only way to call a specific Ltac2 function is to somehow build an AST for the call, and use
you mean something like
Tac2interp.(interp_value empty_environment (GTacRef some_name))? that should work fine
Yeah, that's exactly what I plan to do, except that the expression to evaluate is gonna be a lot more complicated since it requires many arguments to be built (including record values, ...). So that's gonna be a pain, hence my question to see if I missed any other alternative.
I guess I could inject my value into some
CTacExt node, and then have some extra back and forth between OCaml and Ltac2.
you can apply it with
Tac2ffi.(apply (to_closure Tac2interp.(interp_value ...))) [arg1;arg2;...]
args in type valexpr instead of glb_tacexpr
Oh that's perfect actually, I missed the fact that I could do that. Thanks!
Last updated: Nov 29 2023 at 22:01 UTC