{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":18411972,"defaultBranch":"master","name":"FStar","ownerLogin":"FStarLang","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2014-04-03T17:32:49.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/7689927?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1716423275.0","currentOid":""},"activityList":{"items":[{"before":"0e2a116da266fbe1dbb81b414002d0afac6819b3","after":"9820798dcc31cd1ea5c164611a67f58ade0b7655","ref":"refs/heads/master","pushedAt":"2024-05-28T11:57:25.000Z","pushType":"pr_merge","commitsCount":4,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #3308 from mtzguido/3286\n\nFix 3286","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2320859580\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3308\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3308/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3308\">#3308</a> from mtzguido/3286"}},{"before":"96ba8a75698114283b9542dac61a99d2a56c434f","after":"0e2a116da266fbe1dbb81b414002d0afac6819b3","ref":"refs/heads/master","pushedAt":"2024-05-26T00:55:32.000Z","pushType":"pr_merge","commitsCount":9,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #3306 from mtzguido/misc\n\nMisc changes","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2317320818\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3306\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3306/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3306\">#3306</a> from mtzguido/misc"}},{"before":"71e299e311871afa4225ddc404a6c4d83312d0a0","after":"96ba8a75698114283b9542dac61a99d2a56c434f","ref":"refs/heads/master","pushedAt":"2024-05-23T16:12:09.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #3304 from mtzguido/rename_queue\n\nFStar.Queue: rename to FStar.FunctionalQueue","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2313235257\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3304\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3304/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3304\">#3304</a> from mtzguido/rename_queue"}},{"before":"cb9cad37bc53f7b55d6175821c158ead2ecfd3c9","after":null,"ref":"refs/heads/mfrisella_queue","pushedAt":"2024-05-23T00:14:35.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"}},{"before":"8c6a2655bb383a844e63d650c80d513682622af5","after":"71e299e311871afa4225ddc404a6c4d83312d0a0","ref":"refs/heads/master","pushedAt":"2024-05-23T00:14:34.000Z","pushType":"pr_merge","commitsCount":16,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #2958 from FStarLang/mfrisella_queue\n\nQueue library","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1750581733\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/2958\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/2958/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/2958\">#2958</a> from FStarLang/mfrisella_queue"}},{"before":"27e88862e7678b59d8a222d9dfd0993c28abb21a","after":"cb9cad37bc53f7b55d6175821c158ead2ecfd3c9","ref":"refs/heads/mfrisella_queue","pushedAt":"2024-05-23T00:00:39.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"snap","shortMessageHtmlLink":"snap"}},{"before":"bf8b381631cef3a07cc4388d5fb9c5b2a2d53d79","after":"27e88862e7678b59d8a222d9dfd0993c28abb21a","ref":"refs/heads/mfrisella_queue","pushedAt":"2024-05-22T23:36:35.000Z","pushType":"push","commitsCount":1638,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"FStar.Queue: formatting and a few comments","shortMessageHtmlLink":"FStar.Queue: formatting and a few comments"}},{"before":"8ec46c7eaa174fca284a6db50cf0db44f995b2d8","after":"8c6a2655bb383a844e63d650c80d513682622af5","ref":"refs/heads/master","pushedAt":"2024-05-22T22:22:06.000Z","pushType":"pr_merge","commitsCount":10,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #3303 from mtzguido/misc\n\nMisc fixes for error messages","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2311582986\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3303\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3303/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3303\">#3303</a> from mtzguido/misc"}},{"before":"d839af436694c8d9c4ff36640f5a8bcfaffc0e20","after":"8ec46c7eaa174fca284a6db50cf0db44f995b2d8","ref":"refs/heads/master","pushedAt":"2024-05-22T05:20:53.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #3301 from mtzguido/fix_free\n\nSyntax.Free: fix incomplete match","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2309583398\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3301\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3301/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3301\">#3301</a> from mtzguido/fix_free"}},{"before":"1de49aed9db7d0760c866139ec11715b04607f3f","after":"d839af436694c8d9c4ff36640f5a8bcfaffc0e20","ref":"refs/heads/master","pushedAt":"2024-05-21T02:44:23.000Z","pushType":"pr_merge","commitsCount":11,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #3300 from mtzguido/misc_tac\n\nMisc tactics and debugging improvements","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2307111210\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3300\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3300/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3300\">#3300</a> from mtzguido/misc_tac"}},{"before":"1fbdde6cb8da938c0fb8b01ff1924e75c19ab8eb","after":"1de49aed9db7d0760c866139ec11715b04607f3f","ref":"refs/heads/master","pushedAt":"2024-05-19T22:05:00.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #3299 from mtzguido/refext\n\nIntroduce FStar.RefinementExtensionality","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2304748886\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3299\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3299/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3299\">#3299</a> from mtzguido/refext"}},{"before":"d7b8b1cdf347485f5ca7dc078da8c3b16b16bca6","after":"1fbdde6cb8da938c0fb8b01ff1924e75c19ab8eb","ref":"refs/heads/master","pushedAt":"2024-05-19T19:41:14.000Z","pushType":"pr_merge","commitsCount":4,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #3298 from mtzguido/debug\n\nDebug/Options: make sure to restore debugging state after popping options","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2304748707\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3298\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3298/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3298\">#3298</a> from mtzguido/debug"}},{"before":"60844c6deb4501d4808908a434f113a7800a722f","after":"d7b8b1cdf347485f5ca7dc078da8c3b16b16bca6","ref":"refs/heads/master","pushedAt":"2024-05-19T02:11:37.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #3297 from mtzguido/reldelta\n\nRel: make progress checking in head_matches_delta stricter","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2304356635\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3297\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3297/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3297\">#3297</a> from mtzguido/reldelta"}},{"before":"865efb6b95d284c76cb5d4b906c46602c3de35f7","after":"60844c6deb4501d4808908a434f113a7800a722f","ref":"refs/heads/master","pushedAt":"2024-05-17T22:05:59.000Z","pushType":"pr_merge","commitsCount":10,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #3294 from mtzguido/tc_pp\n\nMisc fixes (typeclasses, printing)","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2303623760\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3294\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3294/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3294\">#3294</a> from mtzguido/tc_pp"}},{"before":"15b612499a2f0bfce915ba975ab4ca6c3ba1f369","after":"865efb6b95d284c76cb5d4b906c46602c3de35f7","ref":"refs/heads/master","pushedAt":"2024-05-17T01:00:54.000Z","pushType":"pr_merge","commitsCount":4,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #3293 from mtzguido/3292\n\nPartial fix for 3292","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2301608877\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3293\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3293/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3293\">#3293</a> from mtzguido/3292"}},{"before":"9d7c7002b68217f510c5f2c64761ffc5ec2be2e4","after":"15b612499a2f0bfce915ba975ab4ca6c3ba1f369","ref":"refs/heads/master","pushedAt":"2024-05-17T00:20:46.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #3291 from mtzguido/warn_color\n\nColor warnings yellow, diagnostics blue","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2301133559\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3291\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3291/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3291\">#3291</a> from mtzguido/warn_color"}},{"before":"307d187ded56e43519973d82ad70e2387c49bc98","after":"9d7c7002b68217f510c5f2c64761ffc5ec2be2e4","ref":"refs/heads/master","pushedAt":"2024-05-16T19:11:19.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #3290 from mtzguido/ppinstances\n\nPpinstances","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2301130545\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3290\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3290/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3290\">#3290</a> from mtzguido/ppinstances"}},{"before":"9a1d64c3a8cfbb22363ed90b3cb1bfd79d8ddb5f","after":"307d187ded56e43519973d82ad70e2387c49bc98","ref":"refs/heads/master","pushedAt":"2024-05-16T00:36:21.000Z","pushType":"pr_merge","commitsCount":4,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #3279 from mtzguido/tac_err\n\nTactics: if dump_on_failure is true, do not add Tactic failed prefix","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2270113921\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3279\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3279/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3279\">#3279</a> from mtzguido/tac_err"}},{"before":"23d4ec1068d856aa1e1b3da8effd93e11398500b","after":"9a1d64c3a8cfbb22363ed90b3cb1bfd79d8ddb5f","ref":"refs/heads/master","pushedAt":"2024-05-14T22:52:56.000Z","pushType":"pr_merge","commitsCount":5,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #3289 from mtzguido/errors_misc\n\nMisc error message fixes","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2296532497\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3289\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3289/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3289\">#3289</a> from mtzguido/errors_misc"}},{"before":"2b27936a9d5f5c14ee69f36b3c2a0c203aa8e2cd","after":"23d4ec1068d856aa1e1b3da8effd93e11398500b","ref":"refs/heads/master","pushedAt":"2024-05-14T21:54:16.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #3285 from mtzguido/sizet\n\nSizeT: make SizeT.t a new type","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2278363652\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3285\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3285/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3285\">#3285</a> from mtzguido/sizet"}},{"before":"28fb7ee2ce78634f9157391016dd5290f2481c0e","after":"2b27936a9d5f5c14ee69f36b3c2a0c203aa8e2cd","ref":"refs/heads/master","pushedAt":"2024-05-13T22:54:59.000Z","pushType":"pr_merge","commitsCount":5,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #3288 from mtzguido/misc_error_messages\n\nMisc error message fixes","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2293967563\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3288\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3288/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3288\">#3288</a> from mtzguido/misc_error_messages"}},{"before":"bb9e55a2bf04feef4a26b7f8bdc69fc5e595dc57","after":"28fb7ee2ce78634f9157391016dd5290f2481c0e","ref":"refs/heads/master","pushedAt":"2024-05-13T18:31:05.000Z","pushType":"pr_merge","commitsCount":8,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #3287 from mtzguido/guido_3264\n\nFixing #3264","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2293479038\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3287\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3287/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3287\">#3287</a> from mtzguido/guido_3264"}},{"before":"66e947dad3587d35c3cbb7a24de98ce1008ba444","after":"bb9e55a2bf04feef4a26b7f8bdc69fc5e595dc57","ref":"refs/heads/master","pushedAt":"2024-05-04T01:37:13.000Z","pushType":"push","commitsCount":4,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"snap","shortMessageHtmlLink":"snap"}},{"before":"c990b3cae32f6ed6f10a7d6062c77f9af29150da","after":"bb9e55a2bf04feef4a26b7f8bdc69fc5e595dc57","ref":"refs/heads/guido_misc","pushedAt":"2024-05-04T01:17:52.000Z","pushType":"push","commitsCount":235,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"snap","shortMessageHtmlLink":"snap"}},{"before":"b410b9fa57af079327deb2adc4cd78c344b2ab75","after":"66e947dad3587d35c3cbb7a24de98ce1008ba444","ref":"refs/heads/master","pushedAt":"2024-05-03T15:44:49.000Z","pushType":"pr_merge","commitsCount":5,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #3284 from mtzguido/fix\n\nFix #3266","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2277929098\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3284\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3284/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3284\">#3284</a> from mtzguido/fix"}},{"before":"b332ac1e7a608ace65ae9f16064e5303509f5324","after":"b410b9fa57af079327deb2adc4cd78c344b2ab75","ref":"refs/heads/master","pushedAt":"2024-05-03T07:25:07.000Z","pushType":"pr_merge","commitsCount":9,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Merge pull request #3283 from mtzguido/misc\n\nMisc","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2277044336\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3283\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3283/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3283\">#3283</a> from mtzguido/misc"}},{"before":"3849844bc62687983bce7c4775bd69f7fa212938","after":null,"ref":"refs/heads/nik_restrict_injectivity","pushedAt":"2024-05-01T03:30:30.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"nikswamy","name":null,"path":"/nikswamy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6163359?s=80&v=4"}},{"before":"0996e782012571113969e19bfd7a1674e993ee39","after":"b332ac1e7a608ace65ae9f16064e5303509f5324","ref":"refs/heads/master","pushedAt":"2024-05-01T03:30:29.000Z","pushType":"pr_merge","commitsCount":61,"pusher":{"login":"nikswamy","name":null,"path":"/nikswamy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6163359?s=80&v=4"},"commit":{"message":"Merge pull request #3253 from FStarLang/nik_restrict_injectivity\n\nInjectivity of inductive types revisited","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2249134836\" data-permission-text=\"Title is private\" data-url=\"https://github.com/FStarLang/FStar/issues/3253\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/FStarLang/FStar/pull/3253/hovercard\" href=\"https://github.com/FStarLang/FStar/pull/3253\">#3253</a> from FStarLang/nik_restrict_injectivity"}},{"before":"3b730a9382129727a1ad42d7e05d5239d8c88c31","after":"3849844bc62687983bce7c4775bd69f7fa212938","ref":"refs/heads/nik_restrict_injectivity","pushedAt":"2024-05-01T03:04:10.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mtzguido","name":"Guido Martínez","path":"/mtzguido","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4195583?s=80&v=4"},"commit":{"message":"Fix test\n\nFirst few were failing due to `is_inj` not being found. Use codes\nfor all of them.","shortMessageHtmlLink":"Fix test"}},{"before":"0d8be16a1e7e26be902992f6bbcbc5f84564e489","after":"3b730a9382129727a1ad42d7e05d5239d8c88c31","ref":"refs/heads/nik_restrict_injectivity","pushedAt":"2024-05-01T03:00:24.000Z","pushType":"push","commitsCount":7,"pusher":{"login":"nikswamy","name":null,"path":"/nikswamy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6163359?s=80&v=4"},"commit":{"message":"merge master","shortMessageHtmlLink":"merge master"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEVctW0gA","startCursor":null,"endCursor":null}},"title":"Activity · FStarLang/FStar"}