{"push_id":883036315,"size":9,"distinct_size":9,"ref":"refs/heads/v8.1","head":"cc05daeb5e60d8f8ca34c48361f559d5cad5b485","before":"977afae90c4e2aa974232b0c664346db72aadaa3","commits":[{"sha":"d0b2c015b83f2c53351492b38a597ce6922e5313","author":{"email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr","name":"Hugo Herbelin"},"message":"Revert \"v8.1: Fixing bug #3169 and avoiding anomaly in bug #2885 (vm_compute not\"\n\nThis reverts commit 6d7d0c510ad5f7d3c5a5473c59aab6ac362b685a.","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/d0b2c015b83f2c53351492b38a597ce6922e5313"},{"sha":"bb877e5b54678bc34e4362fcf0315224e7c4f4cc","author":{"email":"2da7cca083ca76060abd20c34814576ca4a06541@inria.fr","name":"Benjamin Gregoire"},"message":"Backporting fix to bug 4157 (vm compute on inductive with more than\n245 constructors).\n\nI had to solve these conflicts:\n\tkernel/cbytegen.ml\n\tkernel/cbytegen.mli\n\tkernel/cemitcodes.ml\n\tkernel/declarations.ml\n\tkernel/mod_typing.ml\n\tkernel/modops.ml\n\tkernel/univ.ml\n\tpretyping/vnorm.ml\n\nCompatibility of compilation with OCaml 3.08 respected.","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/bb877e5b54678bc34e4362fcf0315224e7c4f4cc"},{"sha":"68e1b2b1127fdf73485e8dd7b4ba1bd527cb57e0","author":{"email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr","name":"Hugo Herbelin"},"message":"Tests for fixed critical bugs (sort polymorphism of inductive types +\nguard cofix).","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/68e1b2b1127fdf73485e8dd7b4ba1bd527cb57e0"},{"sha":"384f8d733dae52815fbbc35fd4d1e12785b1c2dd","author":{"email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr","name":"Hugo Herbelin"},"message":"Patch Xavier Leroy for cmxs installation on cygwin (#3843).","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/384f8d733dae52815fbbc35fd4d1e12785b1c2dd"},{"sha":"1537ecef336c54002308c2ba160e5f20058405c8","author":{"email":"c38fa6f5af7dbc000f2995fb690c8f1f1915f07e@85f007b7-540e-0410-9357-904b9bb8a0f7","name":"pboutill"},"message":"Compatibility with compilation with OCaml 4.\n\nPartial cherry-pick of Pierre B.'s patch 517a5dce13.","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/1537ecef336c54002308c2ba160e5f20058405c8"},{"sha":"b5d8f9abef0bd118b7edde87be725c6765bc86dd","author":{"email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr","name":"Hugo Herbelin"},"message":"Fixing OCaml 4.02 compilation (backport of 9c00f3c4f2b6).","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/b5d8f9abef0bd118b7edde87be725c6765bc86dd"},{"sha":"93a99057b1cde8bc56cb8762b03b865e6640f4e6","author":{"email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr","name":"Hugo Herbelin"},"message":"Compatibility ocamldep 4.00.0 (a space has been introduced before the\ncolons, probably unintentionally, while adding options -sort, -all, and\n-one-line to ocamldep in OCaml).","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/93a99057b1cde8bc56cb8762b03b865e6640f4e6"},{"sha":"5d5891789e2bd79c4e060bf716ac5cf55f04d114","author":{"email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr","name":"Hugo Herbelin"},"message":"Supporting compilation of coqide with lablgtk 2.16 and 2.18.\n\nCollapsing new Gtk modifiers to MOD5 for compatibility with lablgtk 2.14.\n\nNot sure that this is the optimal thing to do, but, at least, this\ndoes not seem to be changing the use of CoqIDE wrt to it was when\nusing lablgtk 2.14.\n\nCherry-pick from 8.2 cbc4c50ca.","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/5d5891789e2bd79c4e060bf716ac5cf55f04d114"},{"sha":"cc05daeb5e60d8f8ca34c48361f559d5cad5b485","author":{"email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr","name":"Hugo Herbelin"},"message":"Updating CHANGES.","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/cc05daeb5e60d8f8ca34c48361f559d5cad5b485"}]}