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.018Apr1615149876432131Mar272523212019181613121096428Feb2625242320191817151413121110765432130Jan292321181716151413111098720Dec19181413109654225Nov222120141312111087652131Oct2522181412119620Sep19131198630Aug2928272625242216141312987630Jul221413129753130Jun2928272625242120make 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 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 Coq