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.028Aug1110984327Jul252423222130Jun29141296542131May3019141110985432130Apr292827252419181211626Mar252319201918171097543117Feb161514138432127Jan179813Dec8765430Nov29272624231817161514139231Oct2827729Sep2521206226Aug2522201716151413121110985432130Jul2726232019181615141312875428Jun272610987325May24Merge branch 'robbert/internal_fractional_tweaks' into 'master'better wordingremove spurious spaceMerge branch 'ralf/greatest_fixpoint_paco' into 'master'Improve comment.Minor tweaks to bupd_plain instance and changelog entryInternal fractional tweaks.Add Plain instance for bupdMerge branch 'ralf/fixpoint-confusion' into 'master'fix a lemma being accidentally about the wrong fixpoint...never put Require in the middle of a fileshow that reader_locked and writer_locked exclude each otherGlobal Leamma/Definition doesn't do anythingadd option_fmap_dist_inj lemmaMerge branch 'rw_lock' into 'master'Add reference-counting reader-writer lock implementationMerge branch 'ike/strategy' into 'master'changelogApply suggestionsmake iApply greatest_fixpoint_paco work in more casesNo longer doubly closing commentFix missing ucmra_unit, ucmra_ofeOFix typo in issueAdded comment explaining why these particular constants are set to be expanded.Add Strategy command for cmraAdd a strategy command for ucmra projectionsfix testadd a test documenting recently changed behaviorupdate dependenciesMerge branch 'robbert/iInduction_regression_931' into 'master'Merge branch 'ralf/i-start-proof-hack' into 'master'Fix `iInduction` regression caused by !931.hack: temporarily revert 'iIntros (x)' doing iStartProofiStartProof: print what is not a BI assertionFix bug in iLöb caused by n-ary intros change.Merge branch 'robbert/setoid_docs' into 'master'Tweaks.Improvements by Ralf.Some documentation about `Params` and `Proper`.Merge branch 'ralf/some-included-refl' into 'master'