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.027Nov262220161211986131Oct2927262524222119181311754330Sep2618121031Aug2413112131Jul24231713976543230Jun29282625232221201918171615141312111098654131May30292825242320181715141198743227Apr26252423222120191811109654331Mar28272422212019161514131298765432128Feb2726Heap_lang proofmode tactics: use `wp_expr_simpl` everywhere.Fix bug in `wp_cas_suc`.Add `locC`, the OFE on locations.Bump stdpp.Commonly used variant of `singleton_included` when the element is exclusive.Merge branch 'patch-1' into 'master'Link to HTML sources for easier navigationpublish coqdocsself-compiled ocaml is the new defaultOne more occurence...Do not manually apply TC instances using `refine`.Merge branch 'patch-1' into 'master'Update the link to std++Bump std++ once more.Bump Iris.Bump stdpp.bump stdpp even moreremove no-longer-needed Makefile hackeryBump stdpp.More permissive `gmap_fmap_mono`.Prove that `fmap` on `option` and `gmap` is monotone.Merge branch 'big_opM_union' into 'master'Add `big_opM_union` and `big_sepM_union`.fix Coq 8.9 deprecation warningsBump std++.Property about bigops and replicate.Add missing `Implicit Type` and fix an unbounded variable.Merge branch 'robbert/fork_postcondition' into 'master'Turn global fork postcondition into a predicate over return values.Get rid of `irisG'`.Consistently state equalities in pure lifting lemmas with "post-state" on the LHS.Add CHANGELOG entry.Document `state_interp` and `fork_post`.Remove non-fork versions of pure lifting lemmas.Fine-grained post-conditions for forked-off threads.Merge branch 'robbert/fupd_new_axioms' into 'master'Get rid of useless IntoVal uses.New lemma `step_fupdN_wand`, and use instead of `step_fupdN_mono`.Adapt adequacy of total weakest preconditions to use adequacy of fupd.Allow introduction of `∀` under `|={E1,E2}=>` in case the predicate is plain.