Hi all, I would like to call some Ltac2 code from Ocaml. Let's say for instance I have an Ltac2 function :

```
Ltac2 myfunc (x : bool) (y : int list) : unit := ...
```

Can I call this function from an Ocaml plugin ? And can I pass standard Ocaml values (of type `bool`

and `int list`

) as arguments ?

it's possible

something like

```
let tac = Tac2interp.interp Tac2interp.empty_environment (GTacApp (GTacRef kn, Tac2ffi.[of_bool true; of_list of_int [1; 2; 3]])) in
Proofview.Monad.map Tac2ffi.to_unit tac
```

has type `unit Proofview.tactic`

where `kn`

is the name of your function, buit by doing something like https://github.com/coq/coq/blob/e564bef2404475ec83061cf7bf4b0759d58aca85/plugins/ltac2/tac2quote.ml#L43 I guess

see Tac2interp Tac2ffi etc for more info

if you're not already in tactics you can run the tactic with https://github.com/coq/coq/blob/e564bef2404475ec83061cf7bf4b0759d58aca85/engine/proofview.mli#L158

whether that is a good idea I'm not sure

Thanks ! I'm already in a tactic on the Ocaml side so no worries.

`GTacApp`

expects a list of `glb_tacexpr`

but `Tac2ffi`

produces values of type `Tac2val.valexpr`

, but I can't seem to find how to convert from `valexpr`

to `glb_tacexpr`

?

oh right

something like

```
let tac = Tac2val.apply_val (Tac2interp.eval_global kn) Tac2ffi.[of_bool true; etc] in
```

then

I can't seem to get the kernel name of the Ltac2 constant. I'm building the same kernel name as I would for a standard Coq definition, is that correct ?

Is there a way to access a list of all Ltac2 constants from Ocaml similar to Environ.Globals ?

I'm building the same kernel name as I would for a standard Coq definition, is that correct ?

I don't know what exactly you mean by that so I don't know if it's correct.

Is there a way to access a list of all Ltac2 constants from Ocaml similar to Environ.Globals ?

There's Tac2env.globals

Last updated: Oct 13 2024 at 01:02 UTC