{"push_id":2667148864,"size":36,"distinct_size":19,"ref":"refs/heads/guido_tactics","head":"65c58101d096b9ce3de9c209a6417dbaafd3e590","before":"7aa7f3182b5ced25b69e8a2649574fe2313d51d0","commits":[{"sha":"e6ffc1ab73a2a5a282e62ee2d0f88505a107d492","author":{"name":"Dzomo the everest Yak","email":"76c82b5e467a903462cf94fa82200db51ccc5116@microsoft.com"},"message":"[CI] regenerate hints + ocaml snapshot","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/e6ffc1ab73a2a5a282e62ee2d0f88505a107d492"},{"sha":"82cd3cf51cd065fe2f9d9e1d30a8de7eb36dae2f","author":{"name":"Guido Martínez","email":"649799e19e45e5ec0c0c28ea59e0ff112e8daa79@gmail.com"},"message":"syntax: subst: descend into Meta arg qualifiers","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/82cd3cf51cd065fe2f9d9e1d30a8de7eb36dae2f"},{"sha":"577ab70d55c50c543e8825e8e9b0537041ea7048","author":{"name":"Guido Martínez","email":"649799e19e45e5ec0c0c28ea59e0ff112e8daa79@gmail.com"},"message":"nit","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/577ab70d55c50c543e8825e8e9b0537041ea7048"},{"sha":"4c53b33086f6b157b23a1e9238f6018a865e8bb6","author":{"name":"Guido Martínez","email":"649799e19e45e5ec0c0c28ea59e0ff112e8daa79@gmail.com"},"message":"DsEnv: fix `shorten_module_path` for unqualified lids\n\nFixes #1476","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/4c53b33086f6b157b23a1e9238f6018a865e8bb6"},{"sha":"8f41796caf78013833084922739bcba1f06a02d2","author":{"name":"Guido Martínez","email":"649799e19e45e5ec0c0c28ea59e0ff112e8daa79@gmail.com"},"message":"tc: util: some debugging info in maybe_instantiate","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/8f41796caf78013833084922739bcba1f06a02d2"},{"sha":"6f7aa4a68b39e8cef823ba6793de70755f5cd6e0","author":{"name":"Guido Martínez","email":"649799e19e45e5ec0c0c28ea59e0ff112e8daa79@gmail.com"},"message":"normalizer: implement String.split as a primop","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/6f7aa4a68b39e8cef823ba6793de70755f5cd6e0"},{"sha":"6306278915225b7cd9a1be279a956d181cc56ec5","author":{"name":"Guido Martínez","email":"649799e19e45e5ec0c0c28ea59e0ff112e8daa79@gmail.com"},"message":"reflection: exposing sigelt attributes to Meta-F*","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/6306278915225b7cd9a1be279a956d181cc56ec5"},{"sha":"c9786706c12f9df7763643f729cc8fa1ba9f8876","author":{"name":"Guido Martínez","email":"649799e19e45e5ec0c0c28ea59e0ff112e8daa79@gmail.com"},"message":"nit","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/c9786706c12f9df7763643f729cc8fa1ba9f8876"},{"sha":"707e44dfb8059f27fd77a529a502b1220114f10e","author":{"name":"Guido Martínez","email":"649799e19e45e5ec0c0c28ea59e0ff112e8daa79@gmail.com"},"message":"normalizer: implement String.substring","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/707e44dfb8059f27fd77a529a502b1220114f10e"},{"sha":"e17a6d63eab9960d888910dfddeb5b5264aa75ee","author":{"name":"Guido Martínez","email":"649799e19e45e5ec0c0c28ea59e0ff112e8daa79@gmail.com"},"message":"desugaring: fix delta depth of (@)","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/e17a6d63eab9960d888910dfddeb5b5264aa75ee"},{"sha":"1cb21fd3b184a64181f2db463c32e212f6f739ee","author":{"name":"Guido Martínez","email":"649799e19e45e5ec0c0c28ea59e0ff112e8daa79@gmail.com"},"message":"syntax: embeddings: make sure to gather all arguments when unembedding","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/1cb21fd3b184a64181f2db463c32e212f6f739ee"},{"sha":"cfa9bbf9025520bdfdd679fd8dfbcdc1d5356b61","author":{"name":"Guido Martínez","email":"649799e19e45e5ec0c0c28ea59e0ff112e8daa79@gmail.com"},"message":"debugging info","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/cfa9bbf9025520bdfdd679fd8dfbcdc1d5356b61"},{"sha":"77a806c936600d0594df56004b60d3b725c3e560","author":{"name":"Guido Martínez","email":"649799e19e45e5ec0c0c28ea59e0ff112e8daa79@gmail.com"},"message":"tc: threading the environment through tc_decl\n\nSplicing will modify the desugaring environment","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/77a806c936600d0594df56004b60d3b725c3e560"},{"sha":"8f34048629f08036fa8ac4a0ac8b96e860597906","author":{"name":"Guido Martínez","email":"649799e19e45e5ec0c0c28ea59e0ff112e8daa79@gmail.com"},"message":"DsEnv: (carefully) allow duplicates sigelt in support of splicing","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/8f34048629f08036fa8ac4a0ac8b96e860597906"},{"sha":"21b50aca8f3e4312912c4294fc8d8b4792006664","author":{"name":"Guido Martínez","email":"649799e19e45e5ec0c0c28ea59e0ff112e8daa79@gmail.com"},"message":"tactics: making sure splicing works across modules even without annotating\n\nthanks @lastland","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/21b50aca8f3e4312912c4294fc8d8b4792006664"},{"sha":"6e3ca674795ec4f55d2a93b458bb204e7fae609d","author":{"name":"Guido Martínez","email":"649799e19e45e5ec0c0c28ea59e0ff112e8daa79@gmail.com"},"message":"eta-expanding for F#","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/6e3ca674795ec4f55d2a93b458bb204e7fae609d"},{"sha":"7c459c6dbd334f1e278e5ec691f37138bcd14ae0","author":{"name":"Guido Martínez","email":"649799e19e45e5ec0c0c28ea59e0ff112e8daa79@gmail.com"},"message":"snap","distinct":false,"url":"https://api.github.com/repos/FStarLang/FStar/commits/7c459c6dbd334f1e278e5ec691f37138bcd14ae0"},{"sha":"aa9e2069e3451cfe456755aafde3bf469cde5d92","author":{"name":"Guido Martínez","email":"649799e19e45e5ec0c0c28ea59e0ff112e8daa79@gmail.com"},"message":"tc: attempt to instantiate implicits at the end of applications too\n\ncf. #807","distinct":true,"url":"https://api.github.com/repos/FStarLang/FStar/commits/aa9e2069e3451cfe456755aafde3bf469cde5d92"},{"sha":"9f8dcc139c8da976d038c1fb546e4cf789000a05","author":{"name":"Guido Martínez","email":"649799e19e45e5ec0c0c28ea59e0ff112e8daa79@gmail.com"},"message":"tactics: CanonCommMonoid(Simple): work around implicit instantiation","distinct":true,"url":"https://api.github.com/repos/FStarLang/FStar/commits/9f8dcc139c8da976d038c1fb546e4cf789000a05"},{"sha":"a24cabdd794c6f525ebc1a79d9044cf09ee9c262","author":{"name":"Guido Martínez","email":"649799e19e45e5ec0c0c28ea59e0ff112e8daa79@gmail.com"},"message":"add regression tests for #807","distinct":true,"url":"https://api.github.com/repos/FStarLang/FStar/commits/a24cabdd794c6f525ebc1a79d9044cf09ee9c262"}]}
{"actor":{"display_login":"mtzguido"}}