aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cbytegen.mli
Commit message (Expand)AuthorAge
* [lib] Move global options to their proper place.Gravatar Emilio Jesus Gallego Arias2018-04-02
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* New IR in VM: Clambda.Gravatar Maxime Dénès2018-02-23
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Adds support for the virtual machine to perform reduction of universe polymor...Gravatar Gregory Malecha2015-10-28
* Fix vm compiler to refuse to compile code making use of inductives withGravatar Matthieu Sozeau2015-03-25
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
* Modops: the strengthening functions can work without any env argumentGravatar letouzey2011-05-17
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Nettoyage de code en vue de la release. Plus de Warning: Unused Gravatar aspiwack2007-12-18
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
* Changement des named_contextGravatar gregoire2005-12-02
* compatibility with POWERPCGravatar gregoire2004-11-22
* bug module M:=N avec vmGravatar barras2004-11-17
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 23:49:46 +0000