{"push_id":3047402572,"size":11,"distinct_size":1,"ref":"refs/heads/deprecate-implicit-core-db","head":"ee5aae3dc2a3dfd321f59c25cafbc299a162a94b","before":"3bc223aeb9f4d1285f696e8a22894d0e9433b7cd","commits":[{"sha":"a16cb490545789ad0071d751ff9fbd149c55075d","author":{"name":"Vincent Laporte","email":"5b9500d3ac195ca166d1abfbb700bb9943ca7b7b@fondation-inria.fr"},"message":"[Goptions] More detailed error messages","distinct":false,"url":"https://api.github.com/repos/maximedenes/coq/commits/a16cb490545789ad0071d751ff9fbd149c55075d"},{"sha":"7142034ac3e4d3919d2c1a01df960b79dad70151","author":{"name":"Vincent Laporte","email":"5b9500d3ac195ca166d1abfbb700bb9943ca7b7b@fondation-inria.fr"},"message":"[VM] Fix compilation of int31 eliminators\n\nThe compilation to bytecode of the elimination schemes for int31 must\nhappen after the int31 type is registered to the retroknowledge.\nOtherwise, the “decompint” instruction is not emitted.","distinct":false,"url":"https://api.github.com/repos/maximedenes/coq/commits/7142034ac3e4d3919d2c1a01df960b79dad70151"},{"sha":"81e7467a3db24887e1d4026ee8441846eb09309a","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Only declare univ binders once for mutind","distinct":false,"url":"https://api.github.com/repos/maximedenes/coq/commits/81e7467a3db24887e1d4026ee8441846eb09309a"},{"sha":"7a3b6b644f85489dced02b33712ad21afe0df47d","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Don't declare universe binders for variables.\n\nOtherwise\n~~~\nUnset Strict Universe Declaration.\nSection bar.\n\n  Let baz := Type@{u}.\n\n  Definition k := baz.\nEnd bar.\n\nSection bar.\n\n  Let baz := Type@{u}.\n\n  Definition k' := baz.\nEnd bar.\n~~~\nis broken (and has been since we stopped checking for repeated section names).","distinct":false,"url":"https://api.github.com/repos/maximedenes/coq/commits/7a3b6b644f85489dced02b33712ad21afe0df47d"},{"sha":"620bb4184017a8b720f6937f0cba09e93883e812","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Fix incorrect coq-prog-args in unidecls","distinct":false,"url":"https://api.github.com/repos/maximedenes/coq/commits/620bb4184017a8b720f6937f0cba09e93883e812"},{"sha":"a44b97e3e7f4a302a5255ca9fc57ea0b81a36b7e","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Do not qualify universe names by section path.","distinct":false,"url":"https://api.github.com/repos/maximedenes/coq/commits/a44b97e3e7f4a302a5255ca9fc57ea0b81a36b7e"},{"sha":"ccf995fd843f14ae8dfaf18177be6c2494faea35","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Automatically generate names for universes.\n\nThe names are `uXXX` with `XXX` some number avoiding collision.\n\nNote that there may be some collisions with polymorphic binders, eg\nsomething like\n\n~~~\nSet Universe Polymorphism.\nSection foo.\n  Universe u0.\n  Definition bar := Type.\n  (* bar@{u0} = Type@{u0} but this isn't the section u0 *)\n\n  Definition baz := Type@{u0}. (* this one is the section u0 *)\n  Definition foobar := Eval compute in baz -> Type.\n  (* Type@{u0} -> Type@{u0} but these aren't the same u0 *)\n~~~\nSo maybe we should do a nametab lookup too. This is strictly a\nprinting issue (polymorphic binder names have no other use).\n\nIn the monomorphic case names are qualified by the parent definition\nso it should be fine (barring module/definition collision but we\nalready have those).\n\nNote that there are still unnamed universes as they didn't go through\nUState (eg schemes).","distinct":false,"url":"https://api.github.com/repos/maximedenes/coq/commits/ccf995fd843f14ae8dfaf18177be6c2494faea35"},{"sha":"d384f58e5d910ec14574488f2744011cb09aa932","author":{"name":"Pierre-Marie Pédrot","email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr"},"message":"Merge PR #8760: Automatically generate names for universes.","distinct":false,"url":"https://api.github.com/repos/maximedenes/coq/commits/d384f58e5d910ec14574488f2744011cb09aa932"},{"sha":"9fed572705616e30cb02644adab74270703de389","author":{"name":"Maxime Dénès","email":"729aee223f7fb2b958d2bed8a43ef191a9e9072b@fondation-inria.fr"},"message":"Merge PR #8906: [Goptions] More detailed error messages","distinct":false,"url":"https://api.github.com/repos/maximedenes/coq/commits/9fed572705616e30cb02644adab74270703de389"},{"sha":"94494770254bec236f2f6fe727ae42b79192afe4","author":{"name":"Maxime Dénès","email":"729aee223f7fb2b958d2bed8a43ef191a9e9072b@fondation-inria.fr"},"message":"Merge PR #8886: [VM] Fix compilation of int31 eliminators","distinct":false,"url":"https://api.github.com/repos/maximedenes/coq/commits/94494770254bec236f2f6fe727ae42b79192afe4"},{"sha":"ee5aae3dc2a3dfd321f59c25cafbc299a162a94b","author":{"name":"Maxime Dénès","email":"729aee223f7fb2b958d2bed8a43ef191a9e9072b@fondation-inria.fr"},"message":"Deprecate hint declaration/removal with no specified database\n\nPreviously, hints added without a specified database where implicitly\nput in the \"core\" database, which was discouraged by the user manual\n(because of the lack of modularity of this approach).","distinct":true,"url":"https://api.github.com/repos/maximedenes/coq/commits/ee5aae3dc2a3dfd321f59c25cafbc299a162a94b"}]}
{"actor":{"display_login":"maximedenes"}}