aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2016-06-14Assume totality: dedicated type rather than boolArnaud Spiwack
2015-09-25Add a field in `constant_body` to track constant whose well-foundedness is as...Arnaud Spiwack
2015-09-25Propagate `Guarded` flag from syntax to kernel.Arnaud Spiwack
2015-06-26Add a flag to deactivate guard checking in the kernel.Arnaud Spiwack
2015-06-24Add a corresponding field in `mutual_inductive_entry` (part 2).Arnaud Spiwack
2015-06-24Add a corresponding field in `mutual_inductive_entry` (part 1).Arnaud Spiwack
2015-06-24Add a field in `mutual_inductive_body` to represent mutual inductive whose po...Arnaud Spiwack
2015-06-24Merge branch 'v8.5'Pierre-Marie Pédrot
2015-06-23Less closures makes the GC happy.Pierre-Marie Pédrot
2015-06-23Add a Set Dump Bytecode command for debugging purposes.Maxime Dénès
2015-06-23Document the positivity checker.Arnaud Spiwack
2015-06-22Merge remote-tracking branch 'forge/v8.5'Pierre Boutillier
2015-06-22All invocations to ocaml compilers go through ocamlfindPierre Boutillier
2015-06-15Native compiler: do not catch exceptions not related to dynlink.Maxime Dénès
2015-06-08Fix native compilation of primitive projections. Closes #4210.Maxime Dénès
2015-06-01Making Coq compile with ocp-memprof.Pierre-Marie Pédrot
2015-05-27Fix bug #4159Matthieu Sozeau
2015-05-17Fixing bug #4201: The native compiler is not race-free.Pierre-Marie Pédrot
2015-05-14Disable precompilation for native_compute by default.Guillaume Melquiond
2015-05-12Fix my previous commit on ~polypropPierre Letouzey
2015-05-12Extraction: fix the detection of the "polyprop" situationPierre Letouzey
2015-04-27Fix some ill-typed debugging code in the VM.Guillaume Melquiond
2015-04-22Tactical `progress` compares term up to potentially equalisable universes.Arnaud Spiwack
2015-04-16Fixing bug #4190.Pierre-Marie Pédrot
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-03-25More clever representation of substituted Cemitcode.Pierre-Marie Pédrot
2015-03-25Fully fixing bug #3491 (anomaly when building _rect scheme in theHugo Herbelin
2015-03-24Fixing computation of non-recursively uniform arguments in theHugo Herbelin
2015-03-24Fixing wrong rel_context in checking positivity condition.Hugo Herbelin
2015-03-18More sharing in module substitution.Pierre-Marie Pédrot
2015-03-13Fix compilation with forthcoming Ocaml version 4.03.Arnaud Spiwack
2015-03-03Fix bug #4103: forgot to allow unfolding projections of cofixpoints likeMatthieu Sozeau
2015-02-27Add support so that the type of a match in an inductive type with let-inHugo Herbelin
2015-02-24New function [Constr.equal_with] to compare terms up to variants of [kind_of_...Arnaud Spiwack
2015-02-24Refactoring in [Constr].Arnaud Spiwack
2015-02-23Fix some typos in comments.Guillaume Melquiond
2015-02-21Import (module): Do not force constraints if not ready (Close #4066)Enrico Tassi
2015-02-14Univs: When computing the level of an inductive including indices, letsMatthieu Sozeau
2015-02-12Univs: fix bug #3978: carry around the universe context used toMatthieu Sozeau
2015-02-11Fixing bug #4019, and checker blow-up at once.Pierre-Marie Pédrot
2015-02-11Clarifying the implementation of universe hashconsing.Pierre-Marie Pédrot
2015-02-10Fix typeops ignoring results of check functions with let _, and oneMatthieu Sozeau
2015-02-04Nativelib: catch Unix_error (like no ocamlopt found)Enrico Tassi
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-28Fixing bug #3931.Pierre-Marie Pédrot
2015-01-20Fix a critical bug in machine arithmetic for native compiler.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 10:26:28 +0000