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.026Apr25242322181615149876432131Mar272523212019181613121096428Feb2625242320191817151413121110765432130Jan292321181716151413111098720Dec19181413109654225Nov222120141312111087652131Oct2522181412119620Sep19131198630Aug2928272625242216141312987630Jul221413129753130Jun292827262524Merge branch 'mapsto_ne' into 'master'Add mapsto_mapsto_ne helper lemmaMerge branch 'robbert/coreP' into 'master'More documentation.Improve `coreP` construction.Merge branch 'rename-auth-lemma' into 'master'Rename auth_both_frac_op to auth_both_opupdate dependenciesupdate dependenciesMerge branch 'fix-typos' into 'master'Fix some typos in docsheap_lang lifting: instantiate inv_heapG and inv_heap_invremove unnecessary space in inv_mapsto_own notationmake inv_heap_inv typeclass-opaqueMerge branch 'ralf/gc' into 'master'try different notationMerge branch 'robbert/laterN' into 'master'Merge branch 'fix-notation-3' into 'master'Make use of `▷^` notation in its definition.Merge branch 'jonas/spacing_nit' into 'master'Fixed a spacing issue in metatheory.vFix entailment notations `(⊢@{PROP})` and `(⊣⊢@{PROP} )` etc.add notation for inv_mapsto(_own)?Fix testcase from !404Drop stray spacenotation.v: markup titles in coqdocASCII notation tests: use ASCII notations more in existing codeAdd lemma `subst_map_singleton`.avoid deprecated !#wp_rec_löb: make an assumption persistentMerge branch 'ralf/rec' into 'master'add wp proof rule for recursive functionsavoid (implicit) 'try'changelogrename gc -> inv_heapmove helper lemmas upMake GC locs work with extensional invariants.begin porting GC locations to extensional invariantsmore auto-framingavoid rewriting with a non-rewritable relation