Skip to content
Snippets Groups Projects
Select Git revision
  • atomic
  • auth_update_frag_included
  • fast_string
  • fupd_plain_soundness_no_lc_strong
  • gen_proc
  • gen_proofmode
  • heaplang-form-cleanup
  • heaplang-tex-additions
  • indentation_config
  • insert_alloc_local_update
  • ipm-notation-broken
  • iris-3.0
  • iris-tex-additions
  • iris_style_improvements
  • janno/metacoq
  • janno/monfun
  • jh/bi_morphism
  • jh/done_contradiction
  • jh/independent_metric
  • jh/move_bi_affine
  • 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
29 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.011Jan26Dec21181512109220Nov171411106130Oct2423212017161514131211987654329Sep27262114118130Aug29281110984327Jul252423222130Jun29141296542131May3026211917141110985432130Apr292827252419181211626Mar2523222120192019181710976543117Feb161514138432127Jan179813Dec8765430Nov2927262423181716remove some long-dead filesmastermasterallow testing with Coq 8.20iris-bot: support testing against different Coq versionsMerge branch 'later-laws' into 'master'Add comments explaining intricate later shenanigansremove trailing spaceMerge branch 'ralf/gmap_view_cmra' into 'master'Merge branch 'master' into 'master'update emacs section in editor.mdchangelogMake gmap_view internal and external lemmas consistent.add gmap_view_both_dfrac_validN_total and use it for gmap_view_both_validI_totalexplain why gmap_view_both_dfrac_valid_discrete_total is unidirectionalclarify gmap_view_rel explanationTweaks.port the rest of Iris to the new gmap_viewgeneralize gmap_view for an arbitrary CMRA as valuesMerge branch 'ralf/base_redex' into 'master'changelogfix forgotten renames: head_redex -> base_redex, head_atomic -> base_atomicRefactor proofs of {impl,wand}_timelessSpace.also exclude Coq 8.20 from testingMerge branch 'steps-lb-init' into 'master'Generalize wp_lb_init to steps_lb_0.update dependenciesMerge branch 'egrep' into 'master'egrep -> grep -EMerge branch 'undiscard-laws' into 'master'Merge branch 'robbert/total_adequacy_later' into 'master'Remove needless later in total adequacy.Add CHANGELOG for un-persisting lawsMake dyn_reservation_map follow style for updatePAdd separation logic unpersist update lawsAdd unpersist law for gmap_view fragmentsAdd unpersist laws for authorative parts of fragAdd general/missing lemmas about updatePAdd law for undiscarding dfracsfix typo in changelogMerge branch 'ralf/base_step' into 'master'
Loading