aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2015-10-06Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-05Univs: fix bug #4288, Print Sorted generated backward < constraints.Matthieu Sozeau
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-02Univs: Change intf of push_named_def to return the computed universeMatthieu Sozeau
2015-10-02Univs: refined handling of assumptionsMatthieu Sozeau
2015-10-02Univs: forgot a substitution in mod_typing.Matthieu Sozeau
2015-10-02Univs: correct handling of with in modulesMatthieu Sozeau
2015-10-02Univs: fix bug #4251, handling of template polymorphic constants.Matthieu Sozeau
2015-10-02Univs: fix subtyping of polymorphic parameters.Matthieu Sozeau
2015-10-02Univs: uncovered bug in strengthening of opaque polymorphic definitions.Matthieu Sozeau
2015-10-02Univs: handle side-effects of futures correctly in kernel.Matthieu Sozeau
2015-10-02Univs (kernel) adapt to new invariantsMatthieu Sozeau
2015-10-02Univs: module constraints move to universe contexts as they mightMatthieu Sozeau
2015-10-02Forcing i > Set for global universes (incomplete)Matthieu Sozeau
2015-10-02Universes: enforce Set <= i for all Type occurrences.Matthieu Sozeau
2015-09-25Add a field in `constant_body` to track constant whose well-foundedness is as...Arnaud Spiwack
2015-09-25Merge branch 'v8.5'Pierre-Marie Pédrot
2015-09-25Propagate `Guarded` flag from syntax to kernel.Arnaud Spiwack
2015-09-20Remove unused type_in_type field in safe_env.Maxime Dénès
2015-09-20Fix #3948 Anomaly: unknown constant in Print AssumptionsMaxime Dénès
2015-09-20Better debug printers for module paths.Maxime Dénès
2015-09-14Remove dead code in lazy reduction machine.Maxime Dénès
2015-09-10Assertion checking that invariant enforced by 0f8d1b92 always holds.Maxime Dénès
2015-09-06Merge branch 'v8.5' into trunkMaxime Dénès
2015-09-06Output a warning when conversion compilation failed.Maxime Dénès
2015-09-06Fix a bug in 31 bit arithmetic, leading to failing conversion tests.Maxime Dénès
2015-09-06Fixed critical bug in 31 bit arithmetic of VMCatalin Hritcu
2015-09-06Merge branch 'v8.5'Pierre-Marie Pédrot
2015-09-03print universes when dumping bytecode.Gregory Malecha
2015-09-03Implementing Herbelin's fix for the "NonPar" bugmlasson
2015-08-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-08-02Fixing pop_rel_context.Hugo Herbelin
2015-08-02Reverting 16 last commits, committed mistakenly using the wrong push command.Hugo Herbelin
2015-08-02Fixing pop_rel_contextHugo Herbelin
2015-08-02A patch renaming equal into eq in the module dealing withHugo Herbelin
2015-08-02Adding eq/compare/hash for syntactic view atHugo Herbelin
2015-07-30Followup of 9f81b58551.Pierre-Marie Pédrot
2015-07-30Fixing bug #4289 (hash-consing only user part of constant notHugo Herbelin
2015-07-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-07-29Fixing some English misspelling.Hugo Herbelin
2015-07-27Merge branch 'v8.5'Pierre-Marie Pédrot
2015-07-23a small amount of documentation on the virtual machine.Gregory Malecha
2015-07-22Fix incomplete pattern-matching.Matthieu Sozeau
2015-07-18Merge branch 'v8.5'Pierre-Marie Pédrot
2015-07-16Modules: fix bug #4294Matthieu Sozeau
2015-07-15Univs/Inductive: fix typechecking of casesMatthieu Sozeau
2015-07-10Unused variables reported by OCaml.Hugo Herbelin
2015-07-10Option -type-in-type: added support in checker and making it contaminatingHugo Herbelin
2015-07-10Native compiler: make non-fatal linking errors silent except in debug mode.Maxime Dénès
2015-07-10Native compiler: refactor code handling pre-computed values.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 03:27:22 +0000