summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2021-02-05Notesdenismerigoux_pcmDenis Merigoux
2021-01-13Some updatesDenis Merigoux
2021-01-11Merge branch 'steel' into denismerigoux_pcmDenis Merigoux
2020-12-12propagate framing unification strategy to SteelAtomicAymeric Fromherz
2020-12-11Fix implementation of Steel.Effect after making frame of second computation d...Aymeric Fromherz
2020-12-11Provide better error messages related to scoping restrictions: The tactic now...Aymeric Fromherz
2020-12-09add global rewrite_context and sladmitAymeric Fromherz
2020-12-05Restore DListAymeric Fromherz
2020-12-05disable DList for nowAymeric Fromherz
2020-12-05Propagate framing changes to forkjoin effectAymeric Fromherz
2020-12-05Clean up framing tactic, remove special cases for subcomp, now subsumed by re...Aymeric Fromherz
2020-11-11Merge branch 'steel' into afromher_steel_reduceafromher_steel_reduceAymeric Fromherz
2020-11-11Steel framing: Add user-controlled normalization of termsAymeric Fromherz
2020-11-05fix F#Guido Martínez
2020-11-05snapGuido Martínez
2020-11-05(WIP) tactics: better ranges for implicitsGuido Martínez
2020-11-04an interface for arraysNikhil Swamy
2020-11-03snapNikhil Swamy
2020-11-03merging master inNikhil Swamy
2020-11-03[CI] regenerate hints + ocaml snapshotDzomo the everest Yak
2020-11-02Merge pull request #2178 from FStarLang/afromher_imitate_appAymeric Fromherz
2020-11-02Merge branch 'master' into afromher_imitate_apprefs/pull/2178/headAymeric Fromherz
2020-11-02Merge pull request #2177 from FStarLang/afromher_head_and_argsAymeric Fromherz
2020-11-02Merge branch 'master' into afromher_head_and_argsrefs/pull/2177/headafromher_head_and_argsAymeric Fromherz
2020-11-02[CI] regenerate hints + ocaml snapshotDzomo the everest Yak
2020-11-01[CI] regenerate hints + ocaml snapshotDzomo the everest Yak
2020-10-31[CI] regenerate hints + ocaml snapshotDzomo the everest Yak
2020-10-30[CI] regenerate hints + ocaml snapshotDzomo the everest Yak
2020-10-29[CI] regenerate hints + ocaml snapshotDzomo the everest Yak
2020-10-28Remove obselete Steel.FramingEffectafromher_framing2Aymeric Fromherz
2020-10-28Minor fix in Steel framingAymeric Fromherz
2020-10-28Merge branch 'master' of github:FStarLang/FStar into guido_tacticsGuido Martínez
2020-10-28Add a repro for the second issueGuido Martínez
2020-10-28[CI] regenerate hints + ocaml snapshotDzomo the everest Yak
2020-10-28snapGuido Martínez
2020-10-28tactics: fix a scoping bug in rewriteGuido Martínez
2020-10-28snaprefs/pull/2173/headGuido Martínez
2020-10-28Merge branch 'guido_2169' of github:FStarLang/FStar into masterGuido Martínez
2020-10-28normalizer: remove useless caseGuido Martínez
2020-10-27options: mark --error_contexts as settable in pragmasGuido Martínez
2020-10-27Merge branch 'master' into afromher_imitate_appAymeric Fromherz
2020-10-27snapAymeric Fromherz
2020-10-27Rel: In imitate_app, preserve typing equality between the rhs and the imitationAymeric Fromherz
2020-10-27snapAymeric Fromherz
2020-10-27Add type_of_well_typed in the environmentAymeric Fromherz
2020-10-27DeferredImplicits: Check the real head of an app for a uvarAymeric Fromherz
2020-10-27Rename head_and_args' into head_and_args_fullAymeric Fromherz
2020-10-27[CI] regenerate hints + ocaml snapshotDzomo the everest Yak
2020-10-26snapGuido Martínez
2020-10-26tc: norm: remove a useless caseGuido Martínez
generated by cgit v0.10.2-6-g49f6 at 2024-04-26 15:43:13 (GMT)