aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2015-11-10Fixing a bug in reporting ill-formed constructor.Hugo Herbelin
2015-11-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-04Univs: update refman, better printers for universe contexts.Matthieu Sozeau
2015-10-30Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-29Collect subproof universes in handle_side_effects.Matthieu Sozeau
2015-10-29Cleanup API and comments of 908dcd613Enrico Tassi
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
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-26Merge branch 'v8.5'Pierre-Marie Pédrot
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-19Merge branch 'v8.5'Pierre-Marie Pédrot
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-16Merge branch 'v8.5' into trunkMaxime Dénès
2015-10-16Hashcons bytecode generated by the VM.Pierre-Marie Pédrot
2015-10-16Exporting a purely functional interface to bytecode patching.Pierre-Marie Pédrot
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 00:25:07 +0000