Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit 4364e009 authored by POTTIER Francois's avatar POTTIER Francois


parent f3a89210
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
In the Coq backend, split the largest definitions into smaller
ones. This circumvenents a limitation of vm_compute on 32 bit
machines. This also enables us to perform sharing between
definitions, so that the generated files are much smaller.
......@@ -440,4 +440,3 @@ Fixed behavior of --depend option.
Removed reversed lists from the standard library.
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