aboutsummaryrefslogtreecommitdiff
path: root/kernel/cbytegen.mli
AgeCommit message (Expand)Author
2017-06-16Clean up universes of constants and inductivesAmin Timany
2015-10-28Adds support for the virtual machine to perform reduction of universe polymor...Gregory Malecha
2015-03-25Fix vm compiler to refuse to compile code making use of inductives withMatthieu Sozeau
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-15Correct restriction of vm_compute when handling universe polymorphicMatthieu Sozeau
2011-05-17Modops: the strengthening functions can work without any env argumentletouzey
2011-04-03Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksletouzey
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2007-12-18Nettoyage de code en vue de la release. Plus de Warning: Unused aspiwack
2007-05-11Processor integers + Print assumption (see coqdev mailing list for the aspiwack
2005-12-02Changement des named_contextgregoire
2004-11-22compatibility with POWERPCgregoire
2004-11-17bug module M:=N avec vmbarras
2004-10-20COMMITED BYTECODE COMPILERbarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 13:56:06 +0000