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!