Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
1 result
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.01Oct27Sep252413106543131Aug1031Jul302928272625232221201918167528Jun2625242322212019181714131211109876543231May282726252120191817131211975230Apr292220191514131211827Mar2524232218171514131210986543124Feb232217161514131211105432129Jan282726252320191715141312875424Dec231918161110976Implement a more conservative ident_for_pat_default, which simplifies the iAndDestruct caseAdd tests for iIntuitionistic/iSpatial/iModCore on non-fresh namesadd CHANGELOG entryadd tests for edge cases in iDestruct's name reuseOptimize iDestruct IIntuitionistic/ISpatial/IModalElim casesOptimize iDestruct (splitting cases)relax AsFractional Hint ModeMerge branch 'clarify-proof' into 'master'Clarify funny proof of `tac_twp_cmpxchg_fail`update dependenciesprepare for f_equiv changebump std++; fix for f_equiv improvementstest: ignore line ending differencesget rid of unnecessary OfeMorMerge branch 'ralf/big_sepL_take_drop' into 'master'generalize to big_opL_take_dropMerge branch 'ralf/big-sep_2' into 'master'add big_sep*_sep_2 lemmas for merging bigops via iDestructlemmas to merge a sepL and a sepL2add big_sepL_take_dropMerge branch 'optimize_iIntoEmpValid' into 'master'changelog typographybump std++explain why only Iris timing can be diff'dOptimize iIntoEmpValidMerge branch 'robbert/error_message_autoframe' into 'master'Merge branch 'ralf/wand-format' into 'master'changelogmake binary wand/view shift connectives 'block' formatedMake error message of auto frame more informative.Add tests.Fix `iSpecialize` auto framing error message.add changelog for iris_invG renamemore consistent names for some class projectionsMerge branch 'na_invariants_tweak' into 'master'na_inv: tweak definitionna_invariants: deduplicate proof of fresh_inv_nameMerge branch 'big-op-impl' into 'master'Small tweaksApply 4 suggestion(s) to 1 file(s)