aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* Propagate `Guarded` flag from syntax to kernel.Gravatar Arnaud Spiwack2015-09-25
* Add a flag to deactivate guard checking in the kernel.Gravatar Arnaud Spiwack2015-06-26
* Add a corresponding field in `mutual_inductive_entry` (part 2).Gravatar Arnaud Spiwack2015-06-24
* Add a corresponding field in `mutual_inductive_entry` (part 1).Gravatar Arnaud Spiwack2015-06-24
* Add a field in `mutual_inductive_body` to represent mutual inductive whose po...Gravatar Arnaud Spiwack2015-06-24
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-06-24
|\
| * Less closures makes the GC happy.Gravatar Pierre-Marie Pédrot2015-06-23
| * Add a Set Dump Bytecode command for debugging purposes.Gravatar Maxime Dénès2015-06-23
* | Document the positivity checker.Gravatar Arnaud Spiwack2015-06-23
* | Merge remote-tracking branch 'forge/v8.5'Gravatar Pierre Boutillier2015-06-22
|\|
* | All invocations to ocaml compilers go through ocamlfindGravatar Pierre Boutillier2015-06-22
| * Native compiler: do not catch exceptions not related to dynlink.Gravatar Maxime Dénès2015-06-15
| * Fix native compilation of primitive projections. Closes #4210.Gravatar Maxime Dénès2015-06-08
| * Making Coq compile with ocp-memprof.Gravatar Pierre-Marie Pédrot2015-06-01
|/
* Fix bug #4159Gravatar Matthieu Sozeau2015-05-27
* Fixing bug #4201: The native compiler is not race-free.Gravatar Pierre-Marie Pédrot2015-05-17
* Disable precompilation for native_compute by default.Gravatar Guillaume Melquiond2015-05-14
* Fix my previous commit on ~polypropGravatar Pierre Letouzey2015-05-12
* Extraction: fix the detection of the "polyprop" situationGravatar Pierre Letouzey2015-05-12
* Fix some ill-typed debugging code in the VM.Gravatar Guillaume Melquiond2015-04-27
* Tactical `progress` compares term up to potentially equalisable universes.Gravatar Arnaud Spiwack2015-04-22
* Fixing bug #4190.Gravatar Pierre-Marie Pédrot2015-04-16
* 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
* More clever representation of substituted Cemitcode.Gravatar Pierre-Marie Pédrot2015-03-25
* Fully fixing bug #3491 (anomaly when building _rect scheme in theGravatar Hugo Herbelin2015-03-25
* Fixing computation of non-recursively uniform arguments in theGravatar Hugo Herbelin2015-03-24
* Fixing wrong rel_context in checking positivity condition.Gravatar Hugo Herbelin2015-03-24
* More sharing in module substitution.Gravatar Pierre-Marie Pédrot2015-03-18
* Fix compilation with forthcoming Ocaml version 4.03.Gravatar Arnaud Spiwack2015-03-13
* Fix bug #4103: forgot to allow unfolding projections of cofixpoints likeGravatar Matthieu Sozeau2015-03-03
* Add support so that the type of a match in an inductive type with let-inGravatar Hugo Herbelin2015-02-27
* New function [Constr.equal_with] to compare terms up to variants of [kind_of_...Gravatar Arnaud Spiwack2015-02-24
* Refactoring in [Constr].Gravatar Arnaud Spiwack2015-02-24
* Fix some typos in comments.Gravatar Guillaume Melquiond2015-02-23
* Import (module): Do not force constraints if not ready (Close #4066)Gravatar Enrico Tassi2015-02-21
* Univs: When computing the level of an inductive including indices, letsGravatar Matthieu Sozeau2015-02-14
* Univs: fix bug #3978: carry around the universe context used toGravatar Matthieu Sozeau2015-02-12
* Fixing bug #4019, and checker blow-up at once.Gravatar Pierre-Marie Pédrot2015-02-11
* Clarifying the implementation of universe hashconsing.Gravatar Pierre-Marie Pédrot2015-02-11
* Fix typeops ignoring results of check functions with let _, and oneGravatar Matthieu Sozeau2015-02-10
* Nativelib: catch Unix_error (like no ocamlopt found)Gravatar Enrico Tassi2015-02-04
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Fixing bug #3931.Gravatar Pierre-Marie Pédrot2015-01-28
* Fix a critical bug in machine arithmetic for native compiler.Gravatar Maxime Dénès2015-01-20
* Fix #3379, now that Require inside modules is allowed again.Gravatar Maxime Dénès2015-01-17
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 23:31:52 +0000