How can an OCaml tactic return something else than unit?

Developing plugins
1

Hello everyone.

I am currently trying to write a tactic in Ltac that needs to interact with a data structure remembering Coq terms. As these terms do not necessarily have the same types in Coq, the structure must be handled at the OCaml level (otherwise it would not type correctly in Coq). Thus, I thought about creating two tactics, one to read from the data structure, and another one to add a new entry to it.

However, it looks like the .mlg file describing the new OCaml tactics needs both tactics to be unit Proofview.tactic values. The add tactic has the right type, but the find one needs to return something else than unit. These tactics are meant to be used like this in Ltac:

(* adding entries into the table / map / custom OCaml structure *)
add term1 term_assoc1;
add term2 term_assoc2;
(* in another part of the code, trying to retrieve those elements *)
let my_term_assoc := find my_term in
(* ... *)

The .mlg file contains the following declarations:

TACTIC EXTEND MYPLUGINNAME
| ["find" constr(t)] -> { Plugin.tac_find t }
| ["add" constr(t) constr(t')] -> { Plugin.tac_add t t' }
END

and the associated .mli file contains:

val tac_add : EConstr.t -> EConstr.t -> unit Proofview.tactic
val tac_find : EConstr.t -> EConstr.t Proofview.tactic

The compiler complains about the second one not being unit Proofview.tactic. Maybe I am missing something, and I would be glad to get some help from you. Thanks in advance!

2

Disclaimer: this is waaay harder than it should be.

Due to technical limitations of Ltac, it is not possible to do this with a tactic extension. As a workaround, you can perform this with the internals of ARGUMENT EXTEND instead. I wrote helper functions some time ago precisely to do this, you can freely take inspiration. It’s very intricate stuff though, since it essentially requires to understand the Ltac runtime. I recommend asking on Gitter if you have further questions.

(Since you’re showing interest for the feature, I decided to submit my patches.)