{"push_id":2943301814,"size":268,"distinct_size":5,"ref":"refs/heads/command-atts","head":"326734d4ba594e5d8d8c1a1708635667756e671c","before":"78fe5b7c8579f22a863a519a354317a65d7851e3","commits":[{"sha":"8e88da289d5c96506a9540890ccbd7c22570049c","author":{"name":"Pierre-Marie Pédrot","email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr"},"message":"Fix #8043: Unsafe assignment in checker.\n\nWe use a dedicated mutable constructor to perform a Landin knot.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/8e88da289d5c96506a9540890ccbd7c22570049c"},{"sha":"bef7a78f9b7f2a27d342365107bd9cc992201129","author":{"name":"Matthieu Sozeau","email":"6890fa1d738eb4a06cf1d2634a31d4aac12540b7@mattam.org"},"message":"tacmach: function to gather undef evars of the goal","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/bef7a78f9b7f2a27d342365107bd9cc992201129"},{"sha":"31a52b8e1efc85aead31af1ea4a8106c4c28ffba","author":{"name":"Yishuai Li","email":"edbb844ad022f82a2752f717a43cbf43825a563e@cis.upenn.edu"},"message":"NArith: deprecate N2Bv_gen\n\nUse N2Bv_sized instead.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/31a52b8e1efc85aead31af1ea4a8106c4c28ffba"},{"sha":"46c0756406beea84564625c423e9c5f2307689e1","author":{"name":"Yishuai Li","email":"edbb844ad022f82a2752f717a43cbf43825a563e@cis.upenn.edu"},"message":"Bvector: add BVeq and some notations","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/46c0756406beea84564625c423e9c5f2307689e1"},{"sha":"8d1a5297d55eb0cd02695c81f6dea7aef6f62d31","author":{"name":"Hugo Herbelin","email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr"},"message":"Made names of existential variables interpretable as Ltac variables.\n\nThis concerns e.g. \"?[id]\", \"?[?id]\" or \"?id\" (in terms, not in\npatterns), so that all names occurring in terms are consistently\ninterpreted as ltac names.\n\nMoreover, with that, we can for instance do:\n\nLtac pick x := eexists ?[x].\nGoal exists x, x = 0.\npick foo.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/8d1a5297d55eb0cd02695c81f6dea7aef6f62d31"},{"sha":"ff74451389c13828c644157c960c0d314b389b95","author":{"name":"Enrico Tassi","email":"4f6d07e2b142da7a8716d1cd541ae44f0d273335@inria.fr"},"message":"[ssr] use the right environment in ssrpattern (fix #8454)","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/ff74451389c13828c644157c960c0d314b389b95"},{"sha":"e39c84ff2dc20ce059ee6198e142ca076de8c6cb","author":{"name":"Jason Gross","email":"29bbaec13092d36559e3abc6f27f7d09c395819f@mit.edu"},"message":"Fix Numeral Notations (1/4 - moving things)\n\nMove various things from from numeral.ml to notation.ml and\nnotation.mli; this is required to allow the vernac command to continue\nliving in numeral.ml while preparing to move all of the numeral notation\ninterpretation logic to notation.ml\n\nThis is commit 1/4 in the fix for #8401.\n\nThis is a pure cut/paste commit, modulo adding section-heading comments.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/e39c84ff2dc20ce059ee6198e142ca076de8c6cb"},{"sha":"4888eb7ea720eaa34af8df2769fa300f1ea37173","author":{"name":"Jason Gross","email":"29bbaec13092d36559e3abc6f27f7d09c395819f@mit.edu"},"message":"Fix Numeral Notations (2/4 - exceptions, usr_err)\n\nSwitch to using exceptions rather than user errors.  This will be\nrequired because the machinery for printing constrs is not available in\nnotation.ml, so we move the error message printing to himsg.ml instead.\n\nThis is commit 2/4 in the fix for #8401.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/4888eb7ea720eaa34af8df2769fa300f1ea37173"},{"sha":"ab0015c1c2fce185648da6c0364e6c3eb0515424","author":{"name":"Jason Gross","email":"29bbaec13092d36559e3abc6f27f7d09c395819f@mit.edu"},"message":"Fix Numeral Notations (3/4 - moving more stuff)\n\nMove most of the rest of the stuff from numeral.ml to notation.ml.  Now\nthat we use exceptions to print error messages, all of the\ninterpretation code for numeral notations can be moved to notation.ml.\n\nThis is commit 1/4 in the fix for #8401.\n\nThis is a pure cut/paste commit, modulo fixing name qualifications due\nto moved things, and exposing some stuff in notation.mli (to be removed\nin the next commit, where we finish the numeral notation reworking).","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/ab0015c1c2fce185648da6c0364e6c3eb0515424"},{"sha":"87de52b9b4fd793ee9ddd231633513b6c5070e19","author":{"name":"Jason Gross","email":"29bbaec13092d36559e3abc6f27f7d09c395819f@mit.edu"},"message":"Fix Numeral Notations (4/4 - fixing synch)\n\nThis fixes #8401\nSupersedes / closes #8407\n\nVernacular-command-registered numeral notations now live in the summary,\nand the interpretation function for them is hard-coded.\n\nPlugin-registered numeral notations are still unsynchronized, and only\nthe UIDs of these functions gets synchronized.  I am not 100% sure why\nthis is fine, but the test-suite file working suggests that it is fine.\nI think it is because worker delegation correctly handles\nnon-synchronized state which is declared at `Declare ML Module`-time.\n\nThis final commit changes the synchronization of numeral notations (and\ndeletes no-longer-used declarations in notation.mli that were introduced\ntemporarily in the last commit).  Since the interpretation can now be\ndone in notation.ml, we no longer need to register unique ids for\nnumeral notation (un)interp functions, and can instead synchronize the\nunderlying constants with the document state.  This is the change that\nactually fixes #8401.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/87de52b9b4fd793ee9ddd231633513b6c5070e19"},{"sha":"7dcc01273a18afc2921c567574c76b411c1b63d9","author":{"name":"Jim Fehrle","email":"bf824f37ce1959e4c2f9e2b389d1c2711164087e@sbcglobal.net"},"message":"Use \"rm -rf\" so .coq-native directories are removed.  Fixes #8496.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/7dcc01273a18afc2921c567574c76b411c1b63d9"},{"sha":"4c28e0597067d81f5ee7e8b2b2e668f4d45e973f","author":{"name":"Pierre-Marie Pédrot","email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr"},"message":"Fix printing of abstract universe contexts.\n\nDue to their representation using names, the instance was not properly\ndisplayed.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/4c28e0597067d81f5ee7e8b2b2e668f4d45e973f"},{"sha":"51dad02266f0bea735d496839c559b472bc4553e","author":{"name":"Pierre-Marie Pédrot","email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr"},"message":"Removing calls to AUContext.instance.\n\nWe simply declare the bound universes with their user-facing name in the\nevarmap and call all printing functions on uninstantiated terms. We had to\ntweak the universe name declaring function so that it would work properly\nwith bound universe variables and handle sections correctly.\n\nThis changes the output of polymorphic definitions with unnamed universe\nvariables. Now they are printed as Var(i) instead of the Module.n uid\nthat came from their absolute name.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/51dad02266f0bea735d496839c559b472bc4553e"},{"sha":"aaee23f06e4ac345238cb84edc1c16fafe6b6b3d","author":{"name":"Pierre-Marie Pédrot","email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr"},"message":"Store universe binder names as a mere list of names.\n\nThis is the only information we care about. The printing mechanism is only\ncalled on polymorphic constants, as the naming of global monomorphic levels\nis performed in another module.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/aaee23f06e4ac345238cb84edc1c16fafe6b6b3d"},{"sha":"138f7c628e546775b381fa1f8805acc433839684","author":{"name":"Pierre-Marie Pédrot","email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr"},"message":"Best-effort hack to provide a meaningful name for anonymous bound universes.\n\nThis restores the old behaviour that was printing qualified global names as\na representation of anonymous bound universes, at the cost of a ugly hack.\nIdeally this should be handled by the callers, but for the time being the\ntrade-off is probably OK.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/138f7c628e546775b381fa1f8805acc433839684"},{"sha":"0d7643dabade293696a377dbc1f858dff2d666f4","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Universe binders are Id, not Name. Never print Var.\n\nComes with minor cleanups in exception catching and unnecessary mapi.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/0d7643dabade293696a377dbc1f858dff2d666f4"},{"sha":"4cbbbf0842eab2a996f749957c2e5120d91d6faf","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Add test for univ names of polymorphic inductives in sections.\n\nThis used to print Var (before #8475, even with explicit binders) but\nnow doesn't.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/4cbbbf0842eab2a996f749957c2e5120d91d6faf"},{"sha":"7d4d30ab00ded50e4c15c1b078044ea10dfb2fc1","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Remove hash based univ level compare","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/7d4d30ab00ded50e4c15c1b078044ea10dfb2fc1"},{"sha":"87826c4dc5f2a1125061f37edd95a9e423d256b3","author":{"name":"Andres Erbsen","email":"007872edfbb060115cc56f2a383d7527ac6be172@mit.edu"},"message":"dev/doc/profiling.txt: per-component flame graphs","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/87826c4dc5f2a1125061f37edd95a9e423d256b3"},{"sha":"e186109404b665d79bf441f8d1ccee39cc76b165","author":{"name":"Nick Lewycky","email":"3b9de09f2ff76afe9f0ad4fcae4ff68f52ec7fc4@mxc.ca"},"message":"Fix typo in comment.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/e186109404b665d79bf441f8d1ccee39cc76b165"}]}
{"actor":{"display_login":"SkySkimmer"}}