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.025Sep2413106543131Aug1031Jul302928272625232221201918167528Jun2625242322212019181714131211109876543231May282726252120191817131211975230Apr292220191514131211827Mar2524232218171514131210986543124Feb232217161514131211105432129Jan282726252320191715141312875424Dec2319181611109764test: 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)Add generalized implication lemma for big_sepMadd some missing test name markers to proofmode_irisfix atomic update trailing spacesdefensive formatting: put a box around the proofmode contextupdate dependenciesBump std++ (filter_insert).Merge branch 'ralf/printing' into 'master'changelogsed script: be less strict about spacingMerge branch 'ralf/proofmode-import' into 'master'make logatom printing consistent with new WP/Texan Triple printingimprove view shift and Hoare triple printing