aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
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
2015-01-17Fix #3379, now that Require inside modules is allowed again.Maxime Dénès
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-17Partially revert "Forbid Require inside interactive modules and module types."Maxime Dénès
2015-01-17Univs: Fix alias computation for VMs, computation of normal form ofMatthieu Sozeau
2015-01-17Make native compiler handle universe polymorphic definitions.Maxime Dénès
2015-01-15Correct restriction of vm_compute when handling universe polymorphicMatthieu Sozeau
2015-01-15Make -print-mod-uid accept a list of files.Maxime Dénès
2015-01-13Native compiler: if debug flag not present, remove .native files.Maxime Dénès
2015-01-13Fix bug when discharging universe constraints coming from variablesMatthieu Sozeau
2015-01-13Fix issue in printing due to de Bruijn bug when constructing compatibilityMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 05:57:40 +0000