{"push_id":2748894695,"size":46,"distinct_size":17,"ref":"refs/heads/code-of-conduct","head":"614b8ac1d8ffe34f5a607d16f30642ed3d2958bb","before":"de83bae22b9f239f5ec3665eeff7a09c54b3aeea","commits":[{"sha":"cb219011534a8de24a01ddb007799133cdd2cb0e","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Cleanup reduction effects: they only work on constants.\n\nWe only ever call `reduction_effect_hook` on constants, so there's no\npoint allowing it to be declared with globrefs. There is also no point\nusing a constr map instead of constant map.\n\n(Technically there was a call of the effect hook on projections, but\nthat can never match a globref so it was useless)","distinct":true,"url":"https://api.github.com/repos/Zimmi48/coq/commits/cb219011534a8de24a01ddb007799133cdd2cb0e"},{"sha":"f7d57c92a2fed40099b33fa2d804861c02c95ec6","author":{"name":"Pierre-Marie Pédrot","email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr"},"message":"Fix #7854: Native compilation + flambda trigger SEGFAULT.\n\nWe use a more abstract representation for accumulators in the native\ncompilation scheme, that requires less fiddling with low-level implementation\ndetails. It might be slower though.","distinct":false,"url":"https://api.github.com/repos/Zimmi48/coq/commits/f7d57c92a2fed40099b33fa2d804861c02c95ec6"},{"sha":"84c1ed18d204f9ca478cf2cd26b0e5e9648e5b87","author":{"name":"Jason Gross","email":"29bbaec13092d36559e3abc6f27f7d09c395819f@mit.edu"},"message":"bin,oct,hex conversions positive,Z,N,nat<->string","distinct":false,"url":"https://api.github.com/repos/Zimmi48/coq/commits/84c1ed18d204f9ca478cf2cd26b0e5e9648e5b87"},{"sha":"a697b20f5013abb834cd9dca3fdef2bee53221ad","author":{"name":"Pierre Letouzey","email":"7ec6b8fe66022fc3d68ec74557b90511bdf04dab@inria.fr"},"message":"Ascii.eqb and String.eqb","distinct":false,"url":"https://api.github.com/repos/Zimmi48/coq/commits/a697b20f5013abb834cd9dca3fdef2bee53221ad"},{"sha":"8458615318b2b67a38e356d68926a0838b908fe6","author":{"name":"Jason Gross","email":"29bbaec13092d36559e3abc6f27f7d09c395819f@mit.edu"},"message":"Add Extract Inlined Constant directives for {String,Ascii}.eqb","distinct":false,"url":"https://api.github.com/repos/Zimmi48/coq/commits/8458615318b2b67a38e356d68926a0838b908fe6"},{"sha":"78f59f94975bcf1ca72110415b741369eb812975","author":{"name":"Jason Gross","email":"29bbaec13092d36559e3abc6f27f7d09c395819f@mit.edu"},"message":"Add additional lemmas about {String,Ascii}.eqb\n\nLemma types and names coppied from [Search Z.eqb].","distinct":false,"url":"https://api.github.com/repos/Zimmi48/coq/commits/78f59f94975bcf1ca72110415b741369eb812975"},{"sha":"7f7e567188ea40fb396c1802224b7290b9e873a3","author":{"name":"Jason Gross","email":"29bbaec13092d36559e3abc6f27f7d09c395819f@mit.edu"},"message":"Update CHANGES","distinct":false,"url":"https://api.github.com/repos/Zimmi48/coq/commits/7f7e567188ea40fb396c1802224b7290b9e873a3"},{"sha":"2c96888bd26c293832f442680561fb72f9dc82f5","author":{"name":"Jason Gross","email":"29bbaec13092d36559e3abc6f27f7d09c395819f@mit.edu"},"message":"Add overlay for QuickChick","distinct":false,"url":"https://api.github.com/repos/Zimmi48/coq/commits/2c96888bd26c293832f442680561fb72f9dc82f5"},{"sha":"496d9d4007f59e6114dae9a94ee5a39d241484cf","author":{"name":"Jim","email":"bf824f37ce1959e4c2f9e2b389d1c2711164087e@sbcglobal.net"},"message":"Generate more compact escape sequences by\na) not explicitly setting the default value and\nb) not repeating attributes that are already set.\n\nExample (omitting escape character):\nOld:  E : [92;49;22;23;24;27mev[39;49;22;23;24;27m [39;49;22;23;24;27mn[39;49;22;23;24;27m\nNew:  E : [92mev[0m n\n\n(92 is bright green, the other codes set default attributes).","distinct":false,"url":"https://api.github.com/repos/Zimmi48/coq/commits/496d9d4007f59e6114dae9a94ee5a39d241484cf"},{"sha":"a6131723faa8699e485a88fae8cc2323b82a8461","author":{"name":"Jim Fehrle","email":"bf824f37ce1959e4c2f9e2b389d1c2711164087e@sbcglobal.net"},"message":"Make the out_channel for the log file accessible so tests can write to it (e.g. for debugging)","distinct":false,"url":"https://api.github.com/repos/Zimmi48/coq/commits/a6131723faa8699e485a88fae8cc2323b82a8461"},{"sha":"b4e88c15da749b3edbd56cb70bf280a8e7bbfc3c","author":{"name":"Jasper Hugunin","email":"8cdbb0d40fd8acbe153ed1293f10c1aae908763e@cs.washington.edu"},"message":"Add test for repeated section with same name","distinct":false,"url":"https://api.github.com/repos/Zimmi48/coq/commits/b4e88c15da749b3edbd56cb70bf280a8e7bbfc3c"},{"sha":"8de046df97b1ea391a3f3879c20c74d53c9fba48","author":{"name":"Jim Fehrle","email":"bf824f37ce1959e4c2f9e2b389d1c2711164087e@sbcglobal.net"},"message":"Displays the differences between successive proof steps in coqtop and CoqIDE.\nProof General requires minor changes to make the diffs visible, but this code\nshouldn't break the existing version of PG.\n\nDiffs are computed for the hypotheses and conclusion of the first goal between\nthe old and new proofs. Strings are split into tokens using the Coq lexer,\nthen the list of tokens are diffed using the Myers algorithm.  A fixup routine\n(Pp_diff.shorten_diff_span) shortens the span of the diff result in some cases.\n\nDiffs can be enabled with the Coq commmand \"Set Diffs on|off|removed.\" or\n\"-diffs on|off|removed\" on the OS command line.  The \"on\" option shows only the\nnew item with added text, while \"removed\" shows each modified item twice--once\nwith the old value showing removed text and once with the new value showing\nadded text.\n\nThe highlights use 4 tags to specify the color and underline/strikeout.\nThese are \"diffs.added\", \"diffs.removed\", \"diffs.added.bg\" and \"diffs.removed.bg\".\nThe first two are for added or removed text; the last two are for\nunmodified parts of a modified item.\n\nDiffs that span multiple strings in the Pp are tagged with \"start.diff.*\" and\n\"end.diff.*\", but only on the first and last strings of the span.","distinct":false,"url":"https://api.github.com/repos/Zimmi48/coq/commits/8de046df97b1ea391a3f3879c20c74d53c9fba48"},{"sha":"97069f69ab3a58cc4ccbaa1a835912c6c31dde4d","author":{"name":"Jim Fehrle","email":"bf824f37ce1959e4c2f9e2b389d1c2711164087e@sbcglobal.net"},"message":"Make tokenize_string an optional parameter for diff methods in pp_diffs.\nRemove forward reference to lexer.","distinct":false,"url":"https://api.github.com/repos/Zimmi48/coq/commits/97069f69ab3a58cc4ccbaa1a835912c6c31dde4d"},{"sha":"89a325e9aa761f343f25ed55f3d85f0d5c7f9cfd","author":{"name":"Hugo Herbelin","email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr"},"message":"Merge PR #6597: Binary, Octal, and Hex conversions between [positive], [Z], [N], [nat] and [string]","distinct":false,"url":"https://api.github.com/repos/Zimmi48/coq/commits/89a325e9aa761f343f25ed55f3d85f0d5c7f9cfd"},{"sha":"86632a406ba7d7e9edb6f35ce367585ddd723a2e","author":{"name":"Maxime Dénès","email":"1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@maximedenes.fr"},"message":"Merge PR #8000: Fix #7854: Native compilation + flambda trigger SEGFAULT.","distinct":false,"url":"https://api.github.com/repos/Zimmi48/coq/commits/86632a406ba7d7e9edb6f35ce367585ddd723a2e"},{"sha":"580a026070ab74d05f38e1177632be83a8756566","author":{"name":"Théo Zimmermann","email":"6e6d7530e858430757598f1bcaab6b049abcfdf1@univ-paris-diderot.fr"},"message":"Merge PR #8083: Add test for repeated section with same name","distinct":false,"url":"https://api.github.com/repos/Zimmi48/coq/commits/580a026070ab74d05f38e1177632be83a8756566"},{"sha":"4ab54f3cca76632cb6e258c84abc259e15e9e9f8","author":{"name":"Emilio Jesus Gallego Arias","email":"a1debd7f3d9036292773dd21463eb601946b38d8@x80.org"},"message":"Merge PR #6801: Highlight differences between successive proof steps (color, underline, etc.)","distinct":false,"url":"https://api.github.com/repos/Zimmi48/coq/commits/4ab54f3cca76632cb6e258c84abc259e15e9e9f8"},{"sha":"3cb3ca518b80763624fc643363cd4540ff299cc0","author":{"name":"Emilio Jesus Gallego Arias","email":"a1debd7f3d9036292773dd21463eb601946b38d8@x80.org"},"message":"[ci] Enable native compiler in `egde:flambda` build.\n\nOCaml 4.07.0 should have fixed the (memory eating bug)[https://caml.inria.fr/mantis/view.php?id=7630]","distinct":false,"url":"https://api.github.com/repos/Zimmi48/coq/commits/3cb3ca518b80763624fc643363cd4540ff299cc0"},{"sha":"fb9003c7850c459d7a5981212d8ef87de877bd9f","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Move Heads to pretyping (is_projection will move to Recordops)","distinct":false,"url":"https://api.github.com/repos/Zimmi48/coq/commits/fb9003c7850c459d7a5981212d8ef87de877bd9f"},{"sha":"7817af48a554573fb649028263ecfc0fabe400d8","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Remove useless is_projection in tacred","distinct":false,"url":"https://api.github.com/repos/Zimmi48/coq/commits/7817af48a554573fb649028263ecfc0fabe400d8"}]}
{"actor":{"display_login":"Zimmi48"}}