summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-12-05make F# happyaseem_no_hslAseem Rastogi
2019-12-05Merge branch 'master' into aseem_no_hslAseem Rastogi
2019-12-05snapAseem Rastogi
2019-12-05it's not so simple, nothing is, need to be smarter about Tm_match and coercio...Aseem Rastogi
2019-12-05[CI] regenerate hints + ocaml snapshotDzomo the everest Yak
2019-12-05Merge branch 'master' into aseem_no_hslAseem Rastogi
2019-12-05adding a coercion testcase for conditionally erased typesAseem Rastogi
2019-12-05snapAseem Rastogi
2019-12-05trying to disable coercions for conditionally erased typesAseem Rastogi
2019-12-04swap arguments to avoid prenex polymorphism (with @nikswamy)Tahina Ramananandro
2019-12-04Merge branch 'master' into aseem_no_hslAseem Rastogi
2019-12-04copying some changes from nik_dynamic_regionsAseem Rastogi
2019-12-04tweaking the sub_ptr_value_is lemma to use the witnessed_functorial lemma fro...Aseem Rastogi
2019-12-04implementing the region_lifetime_sub lemma and alloc_and_blit functions for a...Aseem Rastogi
2019-12-04snapAseem Rastogi
2019-12-04default no-op extraction of dynamic regions APIAseem Rastogi
2019-12-04[CI] regenerate hints + ocaml snapshotDzomo the everest Yak
2019-12-03Merge branch 'master' into aseem_misc2Aseem Rastogi
2019-12-03snapAseem Rastogi
2019-12-03relax forcing the guard when typechecking binders with annotated typeAseem Rastogi
2019-12-03[CI] regenerate hints + ocaml snapshotDzomo the everest Yak
2019-12-02[CI] regenerate hints + ocaml snapshotDzomo the everest Yak
2019-12-01[CI] regenerate hints + ocaml snapshotDzomo the everest Yak
2019-11-30[CI] regenerate hints + ocaml snapshotDzomo the everest Yak
2019-11-29[CI] regenerate hints + ocaml snapshotDzomo the everest Yak
2019-11-29Merge branch 'master' into aseem_misc2Aseem Rastogi
2019-11-29array encoding using layered hoare ST effect goes through after strengthening...Aseem Rastogi
2019-11-29Merge branch 'aseem_dynamic_regions_cleanup' of github.com:FStarLang/FStar in...aseem_dynamic_regions_cleanupAseem Rastogi
2019-11-29Merge branch 'master' into aseem_dynamic_regions_cleanupAseem Rastogi
2019-11-28Merge branch 'master' of github:FStarLang/FStarGuido Martínez
2019-11-28Merge branch 'master' into aseem_dynamic_regions_cleanupAseem Rastogi
2019-11-28[CI] regenerate hints + ocaml snapshotDzomo the everest Yak
2019-11-28Whitelist paths for refreshing hintssantiago_refresh_hintsSantiago Zanella-Beguelin
2019-11-28Merge branch 'santiago_refresh_hints'Santiago Zanella-Beguelin
2019-11-28[CI] regenerate hints + ocaml snapshotDzomo the everest Yak
2019-11-28Add hints in ulib/.cache tooSantiago Zanella-Beguelin
2019-11-28[CI] regenerate hints + ocaml snapshotDzomo the everest Yak
2019-11-28Merge branch 'master' into aseem_dynamic_regions_cleanupAseem Rastogi
2019-11-28Revert "weakening precondition of ralloc and ralloc_mm to work with freeable ...Aseem Rastogi
2019-11-28Revert "some fixes"Aseem Rastogi
2019-11-28some fixesAseem Rastogi
2019-11-28Remove outdated script that removed all ulib hintsSantiago Zanella-Beguelin
2019-11-28weakening precondition of ralloc and ralloc_mm to work with freeable heap reg...Aseem Rastogi
2019-11-28removing a temporary fix related to root being not freeableAseem Rastogi
2019-11-28exposing properties of root region in its type, getting rid of an smtpat lemmaAseem Rastogi
2019-11-28[CI] regenerate hints + ocaml snapshotDzomo the everest Yak
2019-11-27snapGuido Martínez
2019-11-27smtencoding: debugging nitGuido Martínez
2019-11-27param: fix for implicitsGuido Martínez
2019-11-27reduce the verbosity of --debug_level LowGuido Martínez
generated by cgit v0.10.2-6-g49f6 at 2024-04-26 11:46:33 (GMT)