aboutsummaryrefslogtreecommitdiff
path: root/kernel/cbytegen.ml
AgeCommit message (Expand)Author
2016-10-26Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-24Fix #5127 Memory corruption with the VMMaxime Dénès
2016-10-19More comments in VM.Maxime Dénès
2016-08-22Use a better data structure for VM compilation of free vars.Pierre-Marie Pédrot
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-06-25[feedback] Add optional ?loc parameter to loggers.Emilio Jesus Gallego Arias
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-01-20Update copyright headers.Maxime Dénès
2015-12-09bug fixes to vm computation + test cases.Gregory Malecha
2015-10-28Refine Gregory Malecha's patch on VM and universe polymorphism.Maxime Dénès
2015-10-28Adds support for the virtual machine to perform reduction of universe polymor...Gregory Malecha
2015-07-29Fixing some English misspelling.Hugo Herbelin
2015-07-05Fix handling of primitive projections in VM.Maxime Dénès
2015-06-23Add a Set Dump Bytecode command for debugging purposes.Maxime Dénès
2015-03-30fix code and bound for SWITCH instruction.Benjamin Gregoire
2015-03-27use a more compact representation of non-constant constructorsBenjamin Gregoire
2015-03-26allows the vm to deal with inductive type with 8388607 constant constructors ...Benjamin Gregoire
2015-03-26Fix bug 4157,Benjamin Gregoire
2015-03-25Fix vm compiler to refuse to compile code making use of inductives withMatthieu Sozeau
2015-02-23Fix some typos in comments.Guillaume Melquiond
2015-01-17Univs: Fix alias computation for VMs, computation of normal form ofMatthieu Sozeau
2015-01-15Correct restriction of vm_compute when handling universe polymorphicMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-11-10Fix #3282: VM confused by let bindings in fixpoints.Maxime Dénès
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-08-25"allows to", like "allowing to", is improperJason Gross
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-14Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it hadPierre-Marie Pédrot
2014-02-26Lazyconstr -> OpaqueproofEnrico Tassi
2013-03-12invalid_arg instead of raise (Invalid_argement ...)letouzey
2013-02-26kernel/declarations becomes a pure mliletouzey
2012-12-19Array.create is deprecatedpboutill
2012-12-14Modulification of identifierppedrot
2012-11-13More monomorphizationsppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-09-14Partial revert of Yann commit in order to use CLib.List when openingppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-08-08Updating headers.herbelin
2012-03-02Noise for nothingpboutill
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-07-30better fix to bug #2319: types are compiled in the env of the bodiesbarras
2010-07-29fixed bug #2105 (compilation of free de Bruijn) and missing lift of predicate...barras
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-05-09Removed $Id$ introduced inadvertently in r13005 (no more $Id$ since r12972)herbelin
2010-05-09Added a few informations about file lineages (for the most part in kernel)herbelin
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:12:18 +0000