{"push_id":2065085561,"size":56,"distinct_size":2,"ref":"refs/heads/master","head":"ac16f4e42695d399514e08abc15f565e0bc926c9","before":"5142cdd4c6fbe83be142b26b22dc8cd05f6d78eb","commits":[{"sha":"9c6dd835f64d80948806428f104b37808a6d7a74","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Port to Coq 8.5.","distinct":false,"url":"https://api.github.com/repos/Template-Coq/template-coq/commits/9c6dd835f64d80948806428f104b37808a6d7a74"},{"sha":"c636911f076571773fff5016908900090fbe6043","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Fix DECLARE PLUGIN statement.\n\nWas required to make tactic quote_term work.","distinct":false,"url":"https://api.github.com/repos/Template-Coq/template-coq/commits/c636911f076571773fff5016908900090fbe6043"},{"sha":"22a5c0b0f32453c0e612fd0d4d00deb222e983e5","author":{"name":"Gregory Malecha","email":"edc927e95ddee0d29a239b42ebcd7a7e557c7f0d@cs.harvard.edu"},"message":"fixing the Makefile.\n\ncloses bug #8","distinct":false,"url":"https://api.github.com/repos/Template-Coq/template-coq/commits/22a5c0b0f32453c0e612fd0d4d00deb222e983e5"},{"sha":"59e3cf7939dc7908cdedc98d0dc816550238326e","author":{"name":"Matthieu Sozeau","email":"385f7ace2b863d21ff523187b1fd442e431592c6@mattam.org"},"message":"Use the arity information of constructors that comes from the\nkernel (not used by the kernel itself though, only the normalized\narity is, mind_nf_lc).","distinct":false,"url":"https://api.github.com/repos/Template-Coq/template-coq/commits/59e3cf7939dc7908cdedc98d0dc816550238326e"},{"sha":"5254a9e7a73352f13890f9a0aa6bca92edc14f77","author":{"name":"Gregory Malecha","email":"edc927e95ddee0d29a239b42ebcd7a7e557c7f0d@gmail.com"},"message":"Merge pull request #15 from mattam82/coq-8.5\n\nUse the arity information of constructors","distinct":false,"url":"https://api.github.com/repos/Template-Coq/template-coq/commits/5254a9e7a73352f13890f9a0aa6bca92edc14f77"},{"sha":"54d2b469de391b94c073dc010d87422364a96b9a","author":{"name":"Gregory Malecha","email":"edc927e95ddee0d29a239b42ebcd7a7e557c7f0d@cs.harvard.edu"},"message":"fixing reduce bug.","distinct":false,"url":"https://api.github.com/repos/Template-Coq/template-coq/commits/54d2b469de391b94c073dc010d87422364a96b9a"},{"sha":"5bccd89e24773f393d3c0a598b035f56e4e9f11c","author":{"name":"Gregory Malecha","email":"edc927e95ddee0d29a239b42ebcd7a7e557c7f0d@cs.harvard.edu"},"message":"reify types of axioms. (closes #9)\n\n- this does not handle polymorphic constants.","distinct":false,"url":"https://api.github.com/repos/Template-Coq/template-coq/commits/5bccd89e24773f393d3c0a598b035f56e4e9f11c"},{"sha":"9161fd2f6795a66c438451496d410e1a54717c56","author":{"name":"Gregory Malecha","email":"edc927e95ddee0d29a239b42ebcd7a7e557c7f0d@cs.harvard.edu"},"message":"adding a clean target.","distinct":false,"url":"https://api.github.com/repos/Template-Coq/template-coq/commits/9161fd2f6795a66c438451496d410e1a54717c56"},{"sha":"95bf7e5de0f32a63aec60c3dcefb00a08c5fed1b","author":{"name":"Gregory Malecha","email":"edc927e95ddee0d29a239b42ebcd7a7e557c7f0d@cs.harvard.edu"},"message":"eliminating the old ocamlbuild files.","distinct":false,"url":"https://api.github.com/repos/Template-Coq/template-coq/commits/95bf7e5de0f32a63aec60c3dcefb00a08c5fed1b"},{"sha":"c071747fa601c027b2e6c83903c26a8df584dd21","author":{"name":"Gregory Malecha","email":"edc927e95ddee0d29a239b42ebcd7a7e557c7f0d@cs.harvard.edu"},"message":"fixing the bug about parsing non-zero level constrs","distinct":false,"url":"https://api.github.com/repos/Template-Coq/template-coq/commits/c071747fa601c027b2e6c83903c26a8df584dd21"},{"sha":"0e54255c7c8e1512948bf2622cc9e02a9e5ef377","author":{"name":"Jason Gross","email":"7298f0ef53f11b987e31cc57a2822f169086d0c9@gmail.com"},"message":"Respect the COQBIN environment variable","distinct":false,"url":"https://api.github.com/repos/Template-Coq/template-coq/commits/0e54255c7c8e1512948bf2622cc9e02a9e5ef377"},{"sha":"fed92ec6d1b4bf119f6cbdf182aac5c873555b2d","author":{"name":"Gregory Malecha","email":"edc927e95ddee0d29a239b42ebcd7a7e557c7f0d@gmail.com"},"message":"Merge pull request #16 from JasonGross/patch-1\n\nRespect the COQBIN environment variable","distinct":false,"url":"https://api.github.com/repos/Template-Coq/template-coq/commits/fed92ec6d1b4bf119f6cbdf182aac5c873555b2d"},{"sha":"e75f3d67cda7674fbc3ad1393fb5af418754038f","author":{"name":"Jason Gross","email":"d3dfe5c5fac772d904d4932d138136d040bb63c7@mit.edu"},"message":"Put the Ast in [Set] rather than [Type]\n\nThis makes it simpler for the datatype to quote itself without messing\naround with universes.","distinct":false,"url":"https://api.github.com/repos/Template-Coq/template-coq/commits/e75f3d67cda7674fbc3ad1393fb5af418754038f"},{"sha":"ac21df43dea490808488604fc844ca512b2f77d2","author":{"name":"Gregory Malecha","email":"edc927e95ddee0d29a239b42ebcd7a7e557c7f0d@gmail.com"},"message":"Merge pull request #19 from JasonGross/coq-8.5+ast-in-set\n\nCherry-pick \"Put the Ast in [Set] rather than [Type]\" into coq-8.5","distinct":false,"url":"https://api.github.com/repos/Template-Coq/template-coq/commits/ac21df43dea490808488604fc844ca512b2f77d2"},{"sha":"c6de18e0ba00980e82f61c98e2348c292f86faa5","author":{"name":"Gregory Malecha","email":"edc927e95ddee0d29a239b42ebcd7a7e557c7f0d@cs.harvard.edu"},"message":"partial denote term tactic from yforester.\n\ncloses #4","distinct":false,"url":"https://api.github.com/repos/Template-Coq/template-coq/commits/c6de18e0ba00980e82f61c98e2348c292f86faa5"},{"sha":"a7c69804c48f974f3325c03da63391189a662c50","author":{"name":"Matthieu Sozeau","email":"385f7ace2b863d21ff523187b1fd442e431592c6@mattam.org"},"message":"Record the arity of each branch in Case constructs (not easily computable otherwise).","distinct":false,"url":"https://api.github.com/repos/Template-Coq/template-coq/commits/a7c69804c48f974f3325c03da63391189a662c50"},{"sha":"76747fc86640848393fb004b59f7ef406b555647","author":{"name":"Gregory Malecha","email":"edc927e95ddee0d29a239b42ebcd7a7e557c7f0d@gmail.com"},"message":"Merge pull request #20 from mattam82/coq-8.5\n\nRecord the arity of each branch in Case constructs","distinct":false,"url":"https://api.github.com/repos/Template-Coq/template-coq/commits/76747fc86640848393fb004b59f7ef406b555647"},{"sha":"de3c4b43dea2f329e4eafe8bff1a0e1a47b9adcb","author":{"name":"Gregory Malecha","email":"edc927e95ddee0d29a239b42ebcd7a7e557c7f0d@cs.harvard.edu"},"message":"fixes to compile with 8.5~beta3","distinct":false,"url":"https://api.github.com/repos/Template-Coq/template-coq/commits/de3c4b43dea2f329e4eafe8bff1a0e1a47b9adcb"},{"sha":"35df610e8651fcf703bce9fa530a15d46a27986c","author":{"name":"Matthieu Sozeau","email":"385f7ace2b863d21ff523187b1fd442e431592c6@mattam.org"},"message":"Add the number of parameters of mutual inductive types in the syntax.\nThe test-suite goes through unchanged.","distinct":false,"url":"https://api.github.com/repos/Template-Coq/template-coq/commits/35df610e8651fcf703bce9fa530a15d46a27986c"},{"sha":"df2bf4c8c6f79ef91534385fa030bd5ea5e4308a","author":{"name":"Matthieu Sozeau","email":"385f7ace2b863d21ff523187b1fd442e431592c6@mattam.org"},"message":"Add an option to cast maximal subterms of sort Prop\n\nCurrently done with a reference and repeated retypechecking of subterms,\nwhich isn't too bad performance-wise according to P. Letouzey.","distinct":false,"url":"https://api.github.com/repos/Template-Coq/template-coq/commits/df2bf4c8c6f79ef91534385fa030bd5ea5e4308a"}]}
{"actor":{"display_login":"mattam82"}}