aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2015-07-09Kernel/Checker: Cleanup fixes of substitutions due to let-ins.Matthieu Sozeau
2015-07-09Kernel: primitive projections handling of let-insMatthieu Sozeau
2015-07-09Improve semantics of -native-compiler flag.Maxime Dénès
2015-07-09Template polymorphism: A bug-fix for Bug #4258mlasson
2015-07-07Univs: bug fix.Matthieu Sozeau
2015-07-06Merge branch 'v8.5' into trunkMaxime Dénès
2015-07-05Fixing documentation (see Maxime's mail on coqdev, July 3).Hugo Herbelin
2015-07-05Fix handling of primitive projections in VM.Maxime Dénès
2015-07-03Fix convertibility of primitive projections for native_compute.Maxime Dénès
2015-07-02Merge branch 'v8.5' into trunkMaxime Dénès
2015-07-02More robust pattern matching on structured constants in VM.Maxime Dénès
2015-07-02Display functions for primitive projections.Maxime Dénès
2015-07-01Further simplification of the graph traversal in Univ.Pierre-Marie Pédrot
2015-06-28Merge branch 'v8.5'Pierre-Marie Pédrot
2015-06-26Share prop/set values in sorts.ml.Matthieu Sozeau
2015-06-26BUGFIX: Three fixes for the price of 1 in sorts.ml:Matthieu Sozeau
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-24Less closures makes the GC happy.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 13:01:58 +0000