aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2016-01-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-11mergeMatej Kosik
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2016-01-11COMMENTS: of "Constr.case_info" type were updated.Matej Kosik
2016-01-11COMMENTS: added to the "Names.inductive" and "Names.constructor" types.Matej Kosik
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-06Merge remote-tracking branch 'origin/v8.5' into trunkGuillaume Melquiond
2016-01-06Protect code against changes in Map interface.Maxime Dénès
2016-01-05Merge remote-tracking branch 'origin/v8.5' into trunkGuillaume Melquiond
2016-01-04Fix handling of side-effects in case of `Opaque side-effects as well.Matthieu Sozeau
2016-01-02Remove some unused functions.Guillaume Melquiond
2016-01-02Avoid warnings about loop indices.Guillaume Melquiond
2016-01-01Fix typos.Guillaume Melquiond
2016-01-01Remove unused open.Guillaume Melquiond
2015-12-31Fix bug #4456, anomaly in handle-side effectsMatthieu Sozeau
2015-12-31Merge branch 'v8.5' into trunkGuillaume Melquiond
2015-12-27Removing dead code.Pierre-Marie Pédrot
2015-12-22COMMENTS: of "Constr.case_info" type were updated.Matej Kosik
2015-12-22COMMENTS: added to the "Names.inductive" and "Names.constructor" types.Matej Kosik
2015-12-22Inclusion of functors with restricted signature is now forbidden (fix #3746)Pierre Letouzey
2015-12-18COMMENTS: added to the "Constr.case_info" type.Matej Kosik
2015-12-18COMMENTS: added to some variants of the "Constr.kind_of_term" type.Matej Kosik
2015-12-18COMMENTS: added to the "Names" module.Matej Kosik
2015-12-17ALPHA-CONVERSION: in the "Reduction" module: clos_fconv --> clos_gen_convMatej Kosik
2015-12-17ALPHA-CONVERSION: in the "Reduction" module: fconv --> gen_convMatej Kosik
2015-12-17CLEANUP: in the Reduction moduleMatej Kosik
2015-12-17CLEANUP: in the Reduction moduleMatej Kosik
2015-12-15Fixing e3cefca41b about supposingly simplifying primitive projectionsHugo Herbelin
2015-12-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-09bug fixes to vm computation + test cases.Gregory Malecha
2015-12-08Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-07Fix some typos.Guillaume Melquiond
2015-12-05Unifying betazeta_applist and prod_applist into a clearer interface.Hugo Herbelin
2015-12-05Slight simplification of the code of primitive projection (in relationHugo Herbelin
2015-12-05Moving extended_rel_vect/extended_rel_list to the kernel.Hugo Herbelin
2015-12-05About building of substitutions from instances.Hugo Herbelin
2015-12-05Experimenting documentation of the Vars.subst functions.Hugo Herbelin
2015-12-05Contracting one extra beta-redex on the fly when typing branches of "match".Hugo Herbelin
2015-12-05A few renaming and simplification in inductive.ml.Hugo Herbelin
2015-12-05Moving three related small half-general half-ad-hoc utility functionsHugo Herbelin
2015-12-01New algorithm for universe cycle detections.Jacques-Henri Jourdan
2015-11-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-27Univs: entirely disallow instantiation of polymorphic constants withMatthieu Sozeau
2015-11-26Merge branch 'v8.5'Pierre-Marie Pédrot
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-20Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-18Fixing fix c71aa6b to primitive projections.Hugo Herbelin
2015-11-18Slightly documenting code for building primitive projections.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 00:04:29 +0000