aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2016-10-24Fix #5127 Memory corruption with the VMMaxime Dénès
2016-10-11Fix for bug #4863, update the Proofview's env withMatthieu Sozeau
2016-09-09Restore native compiler optimizations after they were broken by 9e2ee58.Maxime Dénès
2016-07-25Fix bug #4876: critical bug in guard condition checker.Matthieu Sozeau
2016-07-05Prevent unsafe overwriting of Required modules by toplevel library.Maxime Dénès
2016-07-04congruence: Restrict refreshing to SetMatthieu Sozeau
2016-05-31Fix potential race condition in vm_compute.Guillaume Melquiond
2016-05-19native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Pierre Letouzey
2016-04-27Fixing an incompatility introduced in a404360: kernel conversion wasHugo Herbelin
2016-03-22A patch renaming equal into eq in the module dealing withHugo Herbelin
2016-03-22Adding eq/compare/hash for syntactic view atHugo Herbelin
2016-03-10Primitive projections: protect kernel from erroneous definitions.Matthieu Sozeau
2016-03-10Hashconsing modules.Pierre-Marie Pédrot
2016-03-04This fix is probably not enough to justify that there are no problems withMaxime Dénès
2016-03-04Rename Ephemeron -> CEphemeron.Maxime Dénès
2016-01-26Fixing bde12b70 about reporting ill-formed constructor.Hugo Herbelin
2016-01-20Update copyright headers.Maxime Dénès
2016-01-08Be more verbose about failure to compile libraries to native code.Guillaume Melquiond
2016-01-07Fix a misleading comment for substn_varsMatthieu Sozeau
2016-01-06Protect code against changes in Map interface.Maxime Dénès
2016-01-04Fix handling of side-effects in case of `Opaque side-effects as well.Matthieu Sozeau
2015-12-31Fix bug #4456, anomaly in handle-side effectsMatthieu Sozeau
2015-12-22Inclusion of functors with restricted signature is now forbidden (fix #3746)Pierre Letouzey
2015-12-09bug fixes to vm computation + test cases.Gregory Malecha
2015-12-07Fix some typos.Guillaume Melquiond
2015-11-27Univs: entirely disallow instantiation of polymorphic constants withMatthieu Sozeau
2015-11-23Fix output of universe arcs. (Fix bug #4422)Guillaume Melquiond
2015-11-22Fixing kernel bug in typing match with let-ins in the arity.Hugo Herbelin
2015-11-18Fixing fix c71aa6b to primitive projections.Hugo Herbelin
2015-11-18Slightly documenting code for building primitive projections.Hugo Herbelin
2015-11-18Fixing logical bugs in the presence of let-ins in computiong primitiveHugo Herbelin
2015-11-10Dead code from the commit having introduced primitive projections (a4043608).Hugo Herbelin
2015-11-10Fixing a bug in reporting ill-formed constructor.Hugo Herbelin
2015-11-04Univs: update refman, better printers for universe contexts.Matthieu Sozeau
2015-10-29Collect subproof universes in handle_side_effects.Matthieu Sozeau
2015-10-29Cleanup API and comments of 908dcd613Enrico Tassi
2015-10-28Avoid type checking private_constants (side_eff) again during Qed (#4357).Enrico Tassi
2015-10-28Refine Gregory Malecha's patch on VM and universe polymorphism.Maxime Dénès
2015-10-28Conversion of polymorphic inductive types was incomplete in VM and native.Maxime Dénès
2015-10-28Fix minor typo in native compiler.Maxime Dénès
2015-10-28Adds support for the virtual machine to perform reduction of universe polymor...Gregory Malecha
2015-10-25Safe_typing: add clean_bounded_mod_expr in Include Self of modtype (fix #4331)Pierre Letouzey
2015-10-25Minor module cleanup : error HigherOrderInclude was never happeningPierre Letouzey
2015-10-22Fixing a bug in reporting ill-formed inductive.Hugo Herbelin
2015-10-18Miscellaneous typos, spacing, US spelling in comments or variable names.Hugo Herbelin
2015-10-18Adding a function to mirror decompose_prod_n_assum in that it counts let-ins,Hugo Herbelin
2015-10-16Remove left2right reference from the kernel.Maxime Dénès
2015-10-15Avoid dependency of the pretyper on C code.Maxime Dénès
2015-10-15 Fix #4346 2/2: VM casts were not inferring universe constraints.Maxime Dénès
2015-10-15Fix #4346 1/2: native casts were not inferring universe constraints.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 17:01:46 +0000