aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Expand)Author
2016-01-14Removing constr generic argument.Pierre-Marie Pédrot
2016-01-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-13Fixing #4467 (continued).Hugo Herbelin
2016-01-11mergeMatej Kosik
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2016-01-06Merge remote-tracking branch 'origin/v8.5' into trunkGuillaume Melquiond
2016-01-05Fix order of files in mllib.Maxime Dénès
2016-01-02Simplification of grammar_prod_item type.Pierre-Marie Pédrot
2015-12-21Finer-grained types for toplevel values.Pierre-Marie Pédrot
2015-12-21Using dynamic values in tactic evaluation.Pierre-Marie Pédrot
2015-12-18Tying the loop in tactic printing API.Pierre-Marie Pédrot
2015-12-08Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-07Fixing a minor problem in Makefile.build that was prevening "dev/printers.cma...Matej Kosik
2015-12-07Fix some typos.Guillaume Melquiond
2015-12-05Factorizing unsafe code by relying on the new Dyn module.Pierre-Marie Pédrot
2015-12-05Ensuring that documentation of mli code works in the presence of utf-8Hugo Herbelin
2015-12-03Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-02Update history of revisions.Hugo Herbelin
2015-11-20Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-18MacOS package script: do not fail if link to /Applications already exists.Maxime Dénès
2015-11-16Being more precise and faithful about the origin of the file reportingHugo Herbelin
2015-11-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-13MacOS package script: do not fail if directory _dmg already exists.Maxime Dénès
2015-11-12Script building MacOS package.Maxime Dénès
2015-10-30Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-29Fixing another instance of bug #3267 in eauto, this time in theHugo Herbelin
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-28Refine Gregory Malecha's patch on VM and universe polymorphism.Maxime Dénès
2015-10-28Adds support for the virtual machine to perform reduction of universe polymor...Gregory Malecha
2015-10-27Type-safe Egramml.grammar_prod_item.Pierre-Marie Pédrot
2015-10-26Pcoq entries are given a proper module.Pierre-Marie Pédrot
2015-10-18Adding a notion of monotonous evarmap.Pierre-Marie Pédrot
2015-10-17Dedicated file for universe unification context manipulation.Pierre-Marie Pédrot
2015-10-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-14Reverting modifications in dev/top_printers pushed mistakenly.Pierre-Marie Pédrot
2015-10-14Fixing perfomance issue of auto hints induced by universes.Pierre-Marie Pédrot
2015-10-13Fix some typos.Guillaume Melquiond
2015-10-10Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-09Code cleaning in VM (with Benjamin).Maxime Dénès
2015-10-09Minor typo in universe polymorphism doc.Maxime Dénès
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-02Updating versions history with data from Gérard.Hugo Herbelin
2015-10-02Update the history of versions with recent versions.Hugo Herbelin
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-02Univs: More info for developers.Matthieu Sozeau
2015-09-20Better debug printers for module paths.Maxime Dénès
2015-09-17Merge branch 'v8.5' into trunkMaxime Dénès
2015-09-17Fix Windows installer.Guillaume Melquiond
2015-08-22Merge branch 'v8.5'Pierre-Marie Pédrot