Commit edf21f0c by Jacques-Henri Jourdan


parent 2b06002a
In the Coq backend, we split the largest definitions into smaller
ones. This circumvenient a limitation of vm_compute in 32 bits
machines. This also makes us able to do some sharing between the
definitions, so that the generated files are much smaller.
In the code back-end, generate type annotations when extracting a semantic
value out of the stack. When working with a semantic value of some function
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment