GitLab

Forgetting local variables identifiers

a slightly different representation of coercions
(using trees instead of lists)
bench files for coercions

Now adding the very same coercion is accepted (useful for multiple/transitive use imports)

Minor

Registered exceptions in file coercion.ml

IDE option to show coercions in formulas.
By default this option is set to true

Composition of coercion functions is now labelized

Started a module to contain operations specific to coercions

Treatment of top-level recursive definitions

Erasure of ghost code in statements sequence

div -> ( / )

Minor changes in compile.ml and ocaml_printer.ml

Adding support in drivers for Zarith and the ocaml.mlw file

Working with the extraction driver