Provide generic helper functions to turn Coq terms into ocaml values and vice versa

[lthms]

• Support ascii (char) [prior to this PR]
• Support string (string) [prior to this PR]
• Partial support Z (int)
• Support bool (bool)

[lthms]

Until coq-8.10 is out, I would want to use coq-prelude' signed.t (Definition i63 := signed.t 63`) to deal with bounded signed integers.

What do you think?

[yurug]

I guess that bounded signed/unsigned integers are indeed the adequate types to interact with OCaml-level integers.

Now, to develop certified applications, I would prefer arbitrary precision arithmetic if possible to avoid overflow-related bugs.

The two kinds of integers should probably coexist in a the library.

[lthms]

Since Vincent will need to work with Z, I propose to merge that PR as-is (if you could just have a quick look, @yurug, that would be awesome). Vincent will have to write the conversion from Ocaml to Coq, but it can be a good exercise.

[yurug]

Nothing significant to say. You can merge this even if some refactoring might be needed at some point to make explicit good combinators for deconstruction of Coq values.

[lthms]

Thanks. I will rework it a bit to address your comments, and then merge it.

Thanks your the review! You can tell Vincent this will be ready this afternoon.