Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
Select Git revision
  • borrowck
  • ci/debug
  • ci/for_proph
  • ci/general-contractive
  • ci/hai/siProp
  • ci/janno/strict-tc-resolution
  • ci/msammler/nb_state
  • ci/ralf/Z_of_nat
  • ci/ralf/bi-language
  • 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/iFrame
  • ci/robbert/into_fupd
  • ci/robbert/into_val_pures
  • ci/robbert/kill_locked_value_lambdas
  • 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
36 results
Created with Raphaël 2.2.011Aug10984327Jul252423222130Jun29141296542131May30191614121110985432130Apr292827252419181211626Mar252319201918171097543117Feb161514138432127Jan17129813Dec8765430Nov29272624231817161514139231Oct28271915729Sep2522212019166226Aug2522201716151413121110985432130Jul29never 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'Merge branch 'janno/ltac2-ltac1-lists' into 'master'renameCHANGELOG improvements by Ralf.Address review feedback.Use `_` prefix for private/internal tactics.CHANGELOG.Add `with_ltac1_nil`.Comment.Port `iAssert` to n-ary version.Fix bug in `iInv`.