aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cbytegen.ml
Commit message (Expand)AuthorAge
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\
| * Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-26
| |\
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\| |
| | * Fix #5127 Memory corruption with the VMGravatar Maxime Dénès2016-10-24
| * | More comments in VM.Gravatar Maxime Dénès2016-10-19
* | | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \ \ | |/ / |/| |
* | | Use a better data structure for VM compilation of free vars.Gravatar Pierre-Marie Pédrot2016-08-22
| * | Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| * | Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
|/ /
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* | A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* | [feedback] Add optional ?loc parameter to loggers.Gravatar Emilio Jesus Gallego Arias2016-06-25
* | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
|/
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* bug fixes to vm computation + test cases.Gravatar Gregory Malecha2015-12-09
* Refine Gregory Malecha's patch on VM and universe polymorphism.Gravatar Maxime Dénès2015-10-28
* Adds support for the virtual machine to perform reduction of universe polymor...Gravatar Gregory Malecha2015-10-28
* Fixing some English misspelling.Gravatar Hugo Herbelin2015-07-29
* Fix handling of primitive projections in VM.Gravatar Maxime Dénès2015-07-05
* Add a Set Dump Bytecode command for debugging purposes.Gravatar Maxime Dénès2015-06-23
* fix code and bound for SWITCH instruction.Gravatar Benjamin Gregoire2015-03-30
* use a more compact representation of non-constant constructorsGravatar Benjamin Gregoire2015-03-27
* allows the vm to deal with inductive type with 8388607 constant constructors ...Gravatar Benjamin Gregoire2015-03-26
* Fix bug 4157,Gravatar Benjamin Gregoire2015-03-26
* Fix vm compiler to refuse to compile code making use of inductives withGravatar Matthieu Sozeau2015-03-25
* Fix some typos in comments.Gravatar Guillaume Melquiond2015-02-23
* Univs: Fix alias computation for VMs, computation of normal form ofGravatar Matthieu Sozeau2015-01-17
* Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fix #3282: VM confused by let bindings in fixpoints.Gravatar Maxime Dénès2014-11-10
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it hadGravatar Pierre-Marie Pédrot2014-03-14
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
* invalid_arg instead of raise (Invalid_argement ...)Gravatar letouzey2013-03-12
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
* Array.create is deprecatedGravatar pboutill2012-12-19
* Modulification of identifierGravatar ppedrot2012-12-14
* More monomorphizationsGravatar ppedrot2012-11-13
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
* Partial revert of Yann commit in order to use CLib.List when openingGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Noise for nothingGravatar pboutill2012-03-02
* 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
* better fix to bug #2319: types are compiled in the env of the bodiesGravatar barras2010-07-30