Improve the extraction to OCaml
With this MR we improve the extraction from Coq to OCaml by:
- having all the OCaml functions translated to Coq;
- having a computable version of the extensible types;
- having a try-with which could be extractible;
- having a definition for the sets and maps.
Edited by Guillaume Claret