Xia Li-yao

For builtins pre 4.08 one more trick is to have a standalone raw OCaml module to give a qualifiable name to those types.

Does it not work to fix extraction like ``` Extract Inductive bool => "Bool.t" [ "false" "true" ]. ``` ?

That's a different bug though. Import `ExtrOcamlBasic`.

Here's a dirty hack for the `int` bug, by extracting `Decimal.int` to `uint + uint`. You have to make sure `sum` is extracted (e.g., adding it at the end of...

Another version that avoids depending on the order in which things are extracted, is to put `sum` in an external module, and use qualified names to refer to it: ```...

I'd classify that as working as expected, but it might also be a good idea to generalize `match_con` a little. At the same time, the `match_con` stuff is really meant...

Sadly, generalizing `match_con` to allow arbitrary atoms as constructor tags breaks the current API. I hoped coercions would smooth this out but they don't. We could have the generalized version...

> There is `pretty_error` for `CeresParser.error`, but not `CeresDeserialize.error` yet. Feel free to add it! This issue is more about formatting S-expressions though.

Thanks for working on this! I think it would make sense as a new `.Internal.Error` module. `doctest` is also a good idea!

And it may also be useful to export a couple of generics-related error combinators from the toplevel `Generic.Data` so they can be used by external instances for `Generically` (such as...