{"push_id":3020683755,"size":43,"distinct_size":22,"ref":"refs/heads/sprop","head":"ffd0a8bd1234338f44e51c039f5c32a583da9b08","before":"c65f978211b5dabdf3e0a74287c81f33f71a7e12","commits":[{"sha":"c6cd7c39fc0da9c578cac57c9d06ddb28f0586fd","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Move attributes out of vernacinterp to new attributes module","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/c6cd7c39fc0da9c578cac57c9d06ddb28f0586fd"},{"sha":"34f2cee9142fbd5df04fb1c63719de96609c1579","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Remove location field from attributes\n\nIt was never set, because it makes no sense.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/34f2cee9142fbd5df04fb1c63719de96609c1579"},{"sha":"80785aee7924309ab21b8ce1dcf7964559531216","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"{Vernacentries -> Attributes}.attributes_of_flags","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/80785aee7924309ab21b8ce1dcf7964559531216"},{"sha":"a9f2ba45c7dba54bfd44078587fc6176a5af68d6","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Remove pointless optional arguments to mk_atts","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/a9f2ba45c7dba54bfd44078587fc6176a5af68d6"},{"sha":"8db938764d87cceee6669b339e0f995edd40fc3e","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Command driven attributes.\n\nCommands need to request the attributes they use, with the API\nencouraging them to error on unsupported attributes.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/8db938764d87cceee6669b339e0f995edd40fc3e"},{"sha":"cc95e2f89f88a6e37f1d98ce55e479491c40145a","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Make attributes more general to make defining #[universes(...)] easy","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/cc95e2f89f88a6e37f1d98ce55e479491c40145a"},{"sha":"5c9e05a36fc27413579c49df4994def20811cdff","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Generalize attributes further to get a monad (mostly for [map])\n\nHaving [map] means we can structure attributes when combining them, eg\nget an attribute for [type universe_data = { poly : bool option; template : bool\noption }] from 2 [bool option] attributes.\nUsing the previous representation we would have had to provide the\ninverse function [universe_data -> bool option * bool option] as well.\n\nAn alternate way to get (++) is\n    let (++) (x:'a t) (y:'b t) : ('a*'b) t =\n      x >>= fun xv ->\n      y >>= fun yv ->\n      return (xv,yv)\n\nNot sure if that would be cleaner.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/5c9e05a36fc27413579c49df4994def20811cdff"},{"sha":"e6f90b09efa854a663706a911847b8626485ee07","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Remove evdref style in build_combined_scheme","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/e6f90b09efa854a663706a911847b8626485ee07"},{"sha":"41072ec0482aa18a2a0ccc07814f672f7f85a7bd","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Remove is_universe_polymorphic in indschemes","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/41072ec0482aa18a2a0ccc07814f672f7f85a7bd"},{"sha":"0fa0ad02cb17a19edcd81efc8e41ccdd4f37ffaf","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Remove is_universe_polymorphism in funind\n\nFunind doesn't support polymorphism.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/0fa0ad02cb17a19edcd81efc8e41ccdd4f37ffaf"},{"sha":"f041d16b65d05074e1fea90a654aa3e7f000b6dc","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"rewrite: attributes handle is_univ_poly, is_program_mode","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/f041d16b65d05074e1fea90a654aa3e7f000b6dc"},{"sha":"1bb5e2d8c3149401b6e7513b09c5eba054696477","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Remove incorrect is_universe_polymorphism from modintern","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/1bb5e2d8c3149401b6e7513b09c5eba054696477"},{"sha":"207c6710606c1581a9b3f207769ceaeb99f5c883","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Remove is_universe_polymorphism from printing","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/207c6710606c1581a9b3f207769ceaeb99f5c883"},{"sha":"c7ce8a036e07930793dc4904457188ca97064700","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Simplify use of polymorphism/program globals in attributes","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/c7ce8a036e07930793dc4904457188ca97064700"},{"sha":"1b753da49ea4a10d7779bb50d93bea25157c01bd","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Load doesn't support attributes","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/1b753da49ea4a10d7779bb50d93bea25157c01bd"},{"sha":"9a1e658860b6320830698f197b69694c661ecfa0","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Add comment in stm to unsupport attributes for special commands","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/9a1e658860b6320830698f197b69694c661ecfa0"},{"sha":"1808904b3088595f89c24aa25bffcc54b2b48fda","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Per command attribute parsing for core commands","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/1808904b3088595f89c24aa25bffcc54b2b48fda"},{"sha":"c44080b74f4ea1e4b7ae88dfe5a440364bed3fca","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Universe Polymorphism is a normal attribute modulo the stm (no Flags)","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/c44080b74f4ea1e4b7ae88dfe5a440364bed3fca"},{"sha":"0a478031f0213ef74c3649ea1a8d58aa89e54416","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"coqpp VERNAC EXTEND uses #[ att = attribute; ] syntax\n\nI think for instance the new code in this diff is cleaner and more\nsystematic:\n~~~diff\n VERNAC COMMAND EXTEND VernacDeclareTacticDefinition\n-| [ \"Ltac\" ne_ltac_tacdef_body_list_sep(l, \"with\") ] => {\n+| #[ deprecation; locality; ] [ \"Ltac\" ne_ltac_tacdef_body_list_sep(l, \"with\") ] => {\n     VtSideff (List.map (function\n       | TacticDefinition ({CAst.v=r},_) -> r\n       | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater\n   } -> {\n-         let deprecation, locality = Attributes.(parse Notations.(deprecation ++ locality) atts) in\n          Tacentries.register_ltac (Locality.make_module_locality locality) ?deprecation l;\n   }\n END\n~~~","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/0a478031f0213ef74c3649ea1a8d58aa89e54416"},{"sha":"c73c1ed2315ec01f2f2963b9a40cdf45c5907139","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Add overlays (command driven attributes)","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/c73c1ed2315ec01f2f2963b9a40cdf45c5907139"}]}
{"actor":{"display_login":"SkySkimmer"}}