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.014Apr9876432131Mar272523212019181613121096428Feb2625242320191817151413121110765432130Jan292321181716151413111098720Dec19181413109654225Nov222120141312111087652131Oct2522181412119620Sep19131198630Aug2928272625242216141312987630Jul221413129753130Jun29282726252421201918add 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 relationadd simpler accessorapply review feedbackmake gc a language-independent library like gen_heapsupport (pure) invariants associated with GC locationsGC locationsmove sed script to the end of the changelogMerge branch 'jh/own_big_op' into 'master'Lemmas stating that big ops are commuting with op/sep.Merge branch 'robbert/issue305' into 'master'Merge branch 'fix-intro-forall' into 'master'Add support for naming forall introsFix introducing forall with "%" intro patternfix build on old versions of CoqMerge branch 'ascii-notation' into 'master'CHANGE <intuit> to <#>Apply suggestion to docs/proof_mode.mdRemark about space.adding fixmeascii notation for most iris operators.Merge branch 'ralf/rename_op_core' into 'master'changelog nitsadd sed script