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.024Jul23222130Jun29141296542131May3019141110985432130Apr292827252419181211626Mar252319201918171097543117Feb161514138432127Jan179813Dec8765430Nov29272624231817161514139231Oct2827729Sep2521206226Aug2522201716151413121110985432130Jul2726232019181615141312875428Jun272610987325May242321181716131198764123Apr2012111087623Mar2120Show that for non-step indexed BIs, <pers> can trivially be inhabited.Merge branch 'ike/internal_included' into 'master'CHANGELOG.More tweaks, add comment on hintsTweak proofs.Some missing lemmas.Do all proofs using proof mode.Add derived ≼ connective on the BI level.Merge branch 'robbert/iRevert_names' into 'master'Merge branch 'ralf/option_included' into 'master'Merge branch 'robbert/gmap_local_updates' into 'master'Avoid `@` syntax.Fix typo and improve wording of comment.Merge branch 'robbert/iExFalso_iStartProof' into 'master'Test.Let `iExFalso` perform `iStartProof`.Comment.Add test.Make sure that `iRevert` preserves names and does not invent fresh ones.Merge branch 'local_updates' into 'master'Add local update lemmas for `discrete_fun` and `unit`.Simplify proofs of `gmap` local update lemmas.Add lemma `delete_option_local_update_cancelable`.Add lemma `cmra_opM_fmap_Some`.changelogsimplify proofs and tweak lemma namesmake use of Some inclusion in a few more placesadd some more option_included lemmasRemove redundant and inconsistent parens.Merge branch 'robbert/bi_wand_notation' into 'master'Improve CHANGELOG.Add test.CHANGELOG.Add ∗-∗ as notation in stdpp_scope similar to -∗.Merge branch 'jaemin/mono_nat_alloc' into 'master'add mono_nat_own_alloc_strongMerge branch 'ralf/fractional' into 'master'typos and better commentschangelogfractional lemmas: only keep bidirectional versions