François Bobot

I think a version with `ocaml_any: 'a typ` is not needed because a version with: ``` val ocaml_value : ?format: (Format.formatter -> 'a -> unit) -> string -> 'a typ...

I looked at what it is the path to add such feature in the interpreter, and it boils down to one feature: to be able to get the function pointer...

Is the set of remaining points up-to-date?

Great thanks, I haven't checked ***at all*** but my first hunch was that Dune use the `mt`predicate (thread predicate). Perhaps that has an impact on a library that link differently...

You are right it is a real fix.

It would simplify a lot #643, where one wants to communicate between two stubs, one being [zarith.h] (https://github.com/ocaml/Zarith/blob/master/zarith.h). I believe it is useful for any stubs that provide conversion function...

I'm using it less since I can instantiate in why3 I guess, but it is still a good way to know if some quantification is never instantiated, or which axioms...

I didn't get an error with dune `2.8.2`. Could you test this version? ``` git clone https://github.com/aantron/luv.git --recursive git checkout unix dune build ``` (`make test` is very long, is...

Do you still prefer the same stanza if one accept to include stanzas that the other do not? If people prefer the same stanza, I will move to it once...

Ok I did nearly that but I had to touch all the `stanzas_in` related stuff because it becames `Memo.Lazy.t`. It should be for the better. And it works sufficiently well...