{"push_id":1266937811,"size":135,"distinct_size":19,"ref":"refs/heads/v8.6","head":"7244637f251272c0d0155d49fc7c1af255b7cef8","before":"3a3f11fe1b6c0f059cf2bd0d71aa4deb4a876b26","commits":[{"sha":"166a8c2e15dfa43c3178f70d515dfde1c5f15fad","author":{"name":"Jason Gross","email":"7298f0ef53f11b987e31cc57a2822f169086d0c9@gmail.com"},"message":"Add a renaming of Tacexpr.TacDynamic","distinct":false,"url":"https://api.github.com/repos/matej-kosik/coq/commits/166a8c2e15dfa43c3178f70d515dfde1c5f15fad"},{"sha":"abe34e282ee0a5f9cca3ea9f527b254388de2cf9","author":{"name":"thery","email":"7873182e3357f87752eb4170c89c838a8621a0ec@sophia.inria.fr"},"message":"Bug Fixes : 4851 4858 4880 for nsatz\n\nthe function in_ideal of ideal.ml supposes the list of polynomials\ndoes not contain zero and is duplicate free.\nI force this invariant in the call of in_ideal in nsatz.ml4\n\nthe function clean_pol returns the reduced list plus a list of\nbooleans that indicates which polynomials have been deleted\n\nthe function expand_pol translates back the certificate of\nthe reduced to list to the complete list thanks to the list\nof booleans.\n\nThe fix is quadratic with respect to the input list which should\nbe ok for reasonable usage of nsatz.\nIf there is some performance issue we could improve the in_pol\nfunction.","distinct":false,"url":"https://api.github.com/repos/matej-kosik/coq/commits/abe34e282ee0a5f9cca3ea9f527b254388de2cf9"},{"sha":"8438b97aa5c8d8464ec7389f7992520e2c176ae6","author":{"name":"thery","email":"7873182e3357f87752eb4170c89c838a8621a0ec@sophia.inria.fr"},"message":"improved complexity in nsatz\n\nwe use a hashtable to reduce the complexity of creating\na duplicate-free list.","distinct":false,"url":"https://api.github.com/repos/matej-kosik/coq/commits/8438b97aa5c8d8464ec7389f7992520e2c176ae6"},{"sha":"fea0ea5a210bc56386513b21c305bcaa9ce6f559","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Merge remote-tracking branch 'github/pr/243' into v8.5\n\nWas PR#243: fixing nsatz","distinct":false,"url":"https://api.github.com/repos/matej-kosik/coq/commits/fea0ea5a210bc56386513b21c305bcaa9ce6f559"},{"sha":"2dc63a6f49ea30e175ead4603c93cda4b2bb889b","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Update COPYRIGHT.","distinct":false,"url":"https://api.github.com/repos/matej-kosik/coq/commits/2dc63a6f49ea30e175ead4603c93cda4b2bb889b"},{"sha":"1ef6104cf043ec839059cddfe530a81418a3d474","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Add test file for #4880.","distinct":false,"url":"https://api.github.com/repos/matej-kosik/coq/commits/1ef6104cf043ec839059cddfe530a81418a3d474"},{"sha":"88f4ca3d1798fc28f230f749665bcf48597accc3","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Test file for #4858.","distinct":false,"url":"https://api.github.com/repos/matej-kosik/coq/commits/88f4ca3d1798fc28f230f749665bcf48597accc3"},{"sha":"b0e81d65b85c1846a961196d70cd86ede2993c5b","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Update csdp.cache.","distinct":false,"url":"https://api.github.com/repos/matej-kosik/coq/commits/b0e81d65b85c1846a961196d70cd86ede2993c5b"},{"sha":"72094961d9bd7f0f618d30b2b508d8924336d7b4","author":{"name":"Matthieu Sozeau","email":"385f7ace2b863d21ff523187b1fd442e431592c6@mattam.org"},"message":"Program: Move ProofIrrelevance to Subset.v","distinct":false,"url":"https://api.github.com/repos/matej-kosik/coq/commits/72094961d9bd7f0f618d30b2b508d8924336d7b4"},{"sha":"4c0c4b46993aeb31786d60cb278cfb317dea454e","author":{"name":"Matthieu Sozeau","email":"385f7ace2b863d21ff523187b1fd442e431592c6@mattam.org"},"message":"Add test for pi_eq_proofs.","distinct":false,"url":"https://api.github.com/repos/matej-kosik/coq/commits/4c0c4b46993aeb31786d60cb278cfb317dea454e"},{"sha":"e1661dc9a43b34526437e9bc3029e6320e09f899","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Fix test file for #4858.","distinct":false,"url":"https://api.github.com/repos/matej-kosik/coq/commits/e1661dc9a43b34526437e9bc3029e6320e09f899"},{"sha":"78063b84f46de33de8ad58f80e45a90fa290dcd6","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Add a few fixes in CHANGES that were forgotten.\n\nWe should really automate the generation of the log of fixes for CHANGES.","distinct":false,"url":"https://api.github.com/repos/matej-kosik/coq/commits/78063b84f46de33de8ad58f80e45a90fa290dcd6"},{"sha":"72d9bf028d0cf40cb6c727c69bfbcc15aafc4944","author":{"name":"Pierre Letouzey","email":"7f57ef47d7df4bda39ff7662fedf6b8fbea1832c@inria.fr"},"message":"Makefile: no more .ml4.d hence no more rule to clean them","distinct":false,"url":"https://api.github.com/repos/matej-kosik/coq/commits/72d9bf028d0cf40cb6c727c69bfbcc15aafc4944"},{"sha":"ea25e8bcf64caac66bcbd33457ee91d56e80fea3","author":{"name":"Pierre Letouzey","email":"7f57ef47d7df4bda39ff7662fedf6b8fbea1832c@inria.fr"},"message":".gitignore: no more generated grammar/*.ml files","distinct":false,"url":"https://api.github.com/repos/matej-kosik/coq/commits/ea25e8bcf64caac66bcbd33457ee91d56e80fea3"},{"sha":"605048905db9107a1d4b3c35ce59f5719474f875","author":{"name":"Pierre Letouzey","email":"7f57ef47d7df4bda39ff7662fedf6b8fbea1832c@inria.fr"},"message":"Makefile.build: follow-up of commits by Matej on VERBOSE and READABLE_ML4\n\n - With the ?= construction, we avoid warnings about undefined variables,\n   while tolerating both 'make VERBOSE=1' and 'VERBOSE=1 make'\n\n - Some extra documentation and cleanup","distinct":false,"url":"https://api.github.com/repos/matej-kosik/coq/commits/605048905db9107a1d4b3c35ce59f5719474f875"},{"sha":"3f9215b2b65b902cc52fd540f57f67342401a91f","author":{"name":"Pierre Letouzey","email":"7f57ef47d7df4bda39ff7662fedf6b8fbea1832c@inria.fr"},"message":"Makefile.dev: fix a typo in the 'logic' rule","distinct":false,"url":"https://api.github.com/repos/matej-kosik/coq/commits/3f9215b2b65b902cc52fd540f57f67342401a91f"},{"sha":"55d32c9a017853c2411f894a3ad1a946c628ba9c","author":{"name":"Hugo Herbelin","email":"785e2cbe854d07e62ab9406d6852942772342316@inria.fr"},"message":"Typo.","distinct":false,"url":"https://api.github.com/repos/matej-kosik/coq/commits/55d32c9a017853c2411f894a3ad1a946c628ba9c"},{"sha":"65ba1b36df33a74998240a02fecc1fb80c3eeeee","author":{"name":"Hugo Herbelin","email":"785e2cbe854d07e62ab9406d6852942772342316@inria.fr"},"message":"Fixing printing of evar name in an error message of instantiate.","distinct":false,"url":"https://api.github.com/repos/matej-kosik/coq/commits/65ba1b36df33a74998240a02fecc1fb80c3eeeee"},{"sha":"45250332a1e65d434432940a468312f2ab18a2e8","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Merge branch 'v8.5' into v8.6","distinct":false,"url":"https://api.github.com/repos/matej-kosik/coq/commits/45250332a1e65d434432940a468312f2ab18a2e8"},{"sha":"f64a49297d90851780d453ce12f57ed4d4174438","author":{"name":"Hugo Herbelin","email":"785e2cbe854d07e62ab9406d6852942772342316@inria.fr"},"message":"Fixing a collision about the meta-variable \"..\" in recursive notations.\n\nThis happens when recursive notations are used to define recursive\nnotations.","distinct":false,"url":"https://api.github.com/repos/matej-kosik/coq/commits/f64a49297d90851780d453ce12f57ed4d4174438"}]}
{"actor":{"display_login":"matej-kosik"}}