Skip to content
Snippets Groups Projects
Select Git revision
  • ci/debug
  • ci/for_proph
  • ci/general-contractive
  • ci/hai/siProp
  • ci/hint-cut-revert
  • ci/janno/strict-tc-resolution
  • ci/msammler/nb_state
  • ci/name-mangle
  • ci/ralf/Z_of_nat
  • ci/ralf/bi-language
  • ci/ralf/options-timing
  • ci/robbert/big_op_binder
  • ci/robbert/contractive_ne
  • ci/robbert/coq_bug_7773
  • ci/robbert/faster_iDestruct
  • ci/robbert/faster_iDestruct2
  • ci/robbert/faster_iFresh_joe
  • ci/robbert/frame_fractional
  • ci/robbert/hint_cut_plain
  • ci/robbert/iFrame
  • iris-4.1.0
  • iris-4.0.0
  • iris-3.6.0
  • iris-3.5.0
  • iris-3.4.0
  • iris-3.3.0
  • iris-3.2.0
  • iris-3.1.0
  • iris-3.0.0
  • iris-2.0
  • iris-2.0-rc2
  • iris-2.0-rc1
  • iris-1.1
  • iris-1.0
  • hope-2015-coq-1
  • appendix-1.0.0
  • appendix-1
37 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.08Oct7654329Sep27262114118130Aug29281110984327Jul252423222130Jun29141296542131May3019141110985432130Apr292827252419181211626Mar252319201918171097543117Feb161514138432127Jan17129813Dec8765430Nov29272624231817161514139231Oct28271915729Sep2522212019166226Aug25222017Add `si_pure` for `uPred`.Add reserved notations for `si_pure`.Bump std++.better errors on WP mask mismatchesMerge branch 'robbert/gmap_union' into 'master'Simplify NA-inv protocol.jh/simplify_na_…jh/simplify_na_invMerge branch 'robbert/option_list_Forall2' into 'master'Lemmas and instances for `∪` on `gmap`.CHANGELOG.`Inj`/`Forall` results for `list`/`option` similar to std++.Merge branch 'ralf/fmap_dist_inj' into 'master'Merge branch 'robbert/gmap_ne_rename' into 'master'Merge branch 'robbert/later_map_Next' into 'master'Merge branch 'robbert/cons_dist_inj' into 'master'Rename instances `union_with_proper` → `union_with_ne`,Add lemma `later_map_Next`.Add instance `cons_dist_inj`.Bump std++.Merge branch 'robbert/big_op_plain' into 'master'Remove useless `BiAffine` conditions for big op `Plain` instances.Merge branch 'robbert/string_ident_tweaks' into 'master'More WIP.robbert/iIntro_…robbert/iIntro_iDestruct_freshAdd some types to Ltac2 for string_ident.Avoid duplicating Ltac2 `Option.get`.WIP.update dependenciesenable name manglingci/name-mangleci/name-mangleadd 'iris-bot timing all'frame_and commentMerge branch 'robbert/naming_as' into 'master'Document convention to use `f_as_g` in naming.sed script for logatom changeMerge branch 'ralf/atomic-private-post' into 'master'changelogadjust logatom notation to avoid a conflict with Autosubstatomic: make no-private-post notation consistent with private-post notationatomic: add support for private postconditionawp_apply: dont leave behind ugly goalsMerge branch 'robbert/naming_order' into 'master'Naming convention about lookup/elem_of.