{"push_id":2071439350,"size":159,"distinct_size":11,"ref":"refs/heads/guido_tactics_test","head":"70cb7ab5b2b6594b9ce2875946b0332b562135b7","before":"c7bdca52125418dba0b77c7a84d2252e86ae9567","commits":[{"sha":"b18d503ee660dea6fc36c2315717172a3ef3f811","author":{"name":"Nikhil Swamy","email":"b4d6aa98ae71f168e6de9d5f2e4ec3e236a67237@users.noreply.github.com"},"message":"revising some of the tactics and reflection to better support bv_tac","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/b18d503ee660dea6fc36c2315717172a3ef3f811"},{"sha":"a120396e196a92cd8f1d61cb2087ed0d4ac3675a","author":{"name":"Nikhil Swamy","email":"b4d6aa98ae71f168e6de9d5f2e4ec3e236a67237@users.noreply.github.com"},"message":"Merge remote-tracking branch 'origin/master' into nik_bvtac","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/a120396e196a92cd8f1d61cb2087ed0d4ac3675a"},{"sha":"e4569968c2adcbd241e990fe5159dfd311b0930c","author":{"name":"Nikhil Swamy","email":"b4d6aa98ae71f168e6de9d5f2e4ec3e236a67237@users.noreply.github.com"},"message":"Merge remote-tracking branch 'origin/guido_tactics' into nik_bvtac","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/e4569968c2adcbd241e990fe5159dfd311b0930c"},{"sha":"edf952eaf01dcbc73bee4a76c39b41c963f95886","author":{"name":"Nikhil Swamy","email":"b4d6aa98ae71f168e6de9d5f2e4ec3e236a67237@users.noreply.github.com"},"message":"reverting a change to `maybe_instantiate`","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/edf952eaf01dcbc73bee4a76c39b41c963f95886"},{"sha":"f3f8a7ec8fb19db4f891671cc158e39d66b35b31","author":{"name":"Nikhil Swamy","email":"b4d6aa98ae71f168e6de9d5f2e4ec3e236a67237@users.noreply.github.com"},"message":"making FStar.UIntN.t abstract","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/f3f8a7ec8fb19db4f891671cc158e39d66b35b31"},{"sha":"338ccba95e073c4927d8b8d1c0723bc6137acc89","author":{"name":"Nikhil Swamy","email":"b4d6aa98ae71f168e6de9d5f2e4ec3e236a67237@users.noreply.github.com"},"message":"fixing up the types of shift operators","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/338ccba95e073c4927d8b8d1c0723bc6137acc89"},{"sha":"cf1b677090e9fa7c79ad96705d4ad1ff447ec5e0","author":{"name":"Nikhil Swamy","email":"b4d6aa98ae71f168e6de9d5f2e4ec3e236a67237@users.noreply.github.com"},"message":"update hints","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/cf1b677090e9fa7c79ad96705d4ad1ff447ec5e0"},{"sha":"e21b363c0ecaff2217fe9521dd53e73c297da4d7","author":{"name":"Nikhil Swamy","email":"b4d6aa98ae71f168e6de9d5f2e4ec3e236a67237@users.noreply.github.com"},"message":"***NO_CI*** relax when the Rel.fs is willing to rely on the smt solver to related types; i.e., additionally allow relating terms with different head symbols when at least one of those head symbols is abstract","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/e21b363c0ecaff2217fe9521dd53e73c297da4d7"},{"sha":"bbaac93364a158028d7abc3aca1f4a7d0a5f22a5","author":{"name":"Nikhil Swamy","email":"b4d6aa98ae71f168e6de9d5f2e4ec3e236a67237@users.noreply.github.com"},"message":"***NO_CI*** Merge branch 'nik_bvtac' of github.com:FStarLang/FStar into nik_bvtac","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/bbaac93364a158028d7abc3aca1f4a7d0a5f22a5"},{"sha":"b45846b1a0dbf4d36b1fde5c96e0ca85e3ec304c","author":{"name":"Nikhil Swamy","email":"b4d6aa98ae71f168e6de9d5f2e4ec3e236a67237@users.noreply.github.com"},"message":"***NO_CI*** snap","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/b45846b1a0dbf4d36b1fde5c96e0ca85e3ec304c"},{"sha":"b794a8a1f4a47cf14d6c529ef493accdf631cc2a","author":{"name":"Nikhil Swamy","email":"b4d6aa98ae71f168e6de9d5f2e4ec3e236a67237@users.noreply.github.com"},"message":"***NO_CI*** propagating the Delta_abstract qualifier, which was being dropped along the way during desugaring","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/b794a8a1f4a47cf14d6c529ef493accdf631cc2a"},{"sha":"d097e876817c72cdb02a1ed78baabb349b275eef","author":{"name":"Nikhil Swamy","email":"b4d6aa98ae71f168e6de9d5f2e4ec3e236a67237@users.noreply.github.com"},"message":"snap","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/d097e876817c72cdb02a1ed78baabb349b275eef"},{"sha":"d2ee4f2851ba0d7d291f6fa9eb546e7d3cefa7f2","author":{"name":"Nikhil Swamy","email":"b4d6aa98ae71f168e6de9d5f2e4ec3e236a67237@users.noreply.github.com"},"message":"new hints","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/d2ee4f2851ba0d7d291f6fa9eb546e7d3cefa7f2"},{"sha":"d374a47b11a0e5e159299ddc15b5073e4d3887f3","author":{"name":"Nikhil Swamy","email":"b4d6aa98ae71f168e6de9d5f2e4ec3e236a67237@users.noreply.github.com"},"message":"bump an rlimit (behavior on CI server is different than my local machines)","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/d374a47b11a0e5e159299ddc15b5073e4d3887f3"},{"sha":"2f13017dae8bfb2678e26b34d33023e9aa3480ff","author":{"name":"Nikhil Swamy","email":"b4d6aa98ae71f168e6de9d5f2e4ec3e236a67237@users.noreply.github.com"},"message":"be more explicit in a flaky proof","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/2f13017dae8bfb2678e26b34d33023e9aa3480ff"},{"sha":"9a7e75b28a9a5198cb831151149ffd5b90abe2a8","author":{"name":"Nikhil Swamy","email":"b4d6aa98ae71f168e6de9d5f2e4ec3e236a67237@users.noreply.github.com"},"message":"revised FStar.IntN.fstp also; some progress in TestBV","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/9a7e75b28a9a5198cb831151149ffd5b90abe2a8"},{"sha":"47703c438793e62ad91d768c06b46214dc29b8b3","author":{"name":"Nikhil Swamy","email":"b4d6aa98ae71f168e6de9d5f2e4ec3e236a67237@users.noreply.github.com"},"message":"disable a failing test","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/47703c438793e62ad91d768c06b46214dc29b8b3"},{"sha":"cfb819fc0149c73be5a385dd2d5d28ded4b5c66a","author":{"name":"Nikhil Swamy","email":"b4d6aa98ae71f168e6de9d5f2e4ec3e236a67237@users.noreply.github.com"},"message":"revising FStar.[U]IntN.fstp to unfold the constant n","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/cfb819fc0149c73be5a385dd2d5d28ded4b5c66a"},{"sha":"3494cb86f2f406894d4fa2d18f5e89630ad9faf0","author":{"name":"Nikhil Swamy","email":"b4d6aa98ae71f168e6de9d5f2e4ec3e236a67237@users.noreply.github.com"},"message":"new hints","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/3494cb86f2f406894d4fa2d18f5e89630ad9faf0"},{"sha":"392523186bb37b039d6b88a9974e0f8f701afa1a","author":{"name":"Nikhil Swamy","email":"b4d6aa98ae71f168e6de9d5f2e4ec3e236a67237@users.noreply.github.com"},"message":"simplifying `b2t true` and `b2t false`","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/392523186bb37b039d6b88a9974e0f8f701afa1a"}]}
{"actor":{"display_login":"mtzguido"}}