aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
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
2015-10-15Warn user when bytecode compilation fails.Maxime Dénès
2015-10-15Remove now useless exception handler in default conversion.Maxime Dénès
2015-10-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-15Fix detection of ties in oracle_order.Guillaume Melquiond
2015-10-14Univs: inductives, remove unneeded testMatthieu Sozeau
2015-10-14Temporary fix: kernel conversion needs to ignore l2r flag.Maxime Dénès
2015-10-14Remove reference to default conversion function inside the kernel.Maxime Dénès
2015-10-14Remove -vm flag of coqtop.Maxime Dénès
2015-10-14Remove unused infos structure in VM.Maxime Dénès
2015-10-14Make interpreter of PROJ simpler by not using the stack.Guillaume Melquiond
2015-10-14Remove some unused variables.Guillaume Melquiond
2015-10-14Fix some typos.Guillaume Melquiond
2015-10-13Fix some typos.Guillaume Melquiond
2015-10-12Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-12Univs: be more restrictive for template polymorphic constants: onlyMatthieu Sozeau
2015-10-12Gather VM tags in Cbytecodes.Maxime Dénès
2015-10-10Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-09Complete handling of primitive projections in VM.Maxime Dénès
2015-10-09Code cleaning in VM (with Benjamin).Maxime Dénès
2015-10-09Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-08Univs: fix bug #3807Matthieu Sozeau
2015-10-08Proof using: let-in policy, optional auto-clear, forward closure*Enrico Tassi
2015-10-08term_typing: strengthen discharging codeEnrico Tassi
2015-10-06Splitting kernel universe code in two modules.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 19:58:16 +0000