Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
Select Git revision
  • arrays
  • atomic
  • atomic_resolve_alternative
  • cas_resolve
  • ci/3.1.0
  • ci/debug
  • ci/disable-ltac-backtrace
  • ci/janno/debug-opam
  • ci/janno/vmcast
  • ci/joe/compact_ipm
  • ci/maximedenes/instance-nobody-open-proof
  • ci/prophecy
  • ci/ralf/ci
  • ci/ralf/pm_red
  • ci/robbert/into_val_pures
  • ci/robbert/kill_locked_value_lambdas
  • ci/robbert/tc_opaque
  • ci/stability
  • ci/value_constructor
  • fast_string
  • 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
30 results
Created with Raphaël 2.2.08Mar765432128Feb27262524232221201918161514131298763231Jan302927252423222120191816131211107331Dec30292322212019181514131211108765432130Nov292827262423222120181615Prove `<absorb> □ P ⊣⊢ <pers> P` and use it to refactor some stuff.Make `of_expr` more consistent with Ltac version.Add missing branch to `iStartProof`.also test wandRevert "Use implication in core so that we can test it.", add a dedicated testUse implication in core so that we can test it.absorbingly_and → absorbingly_and_1Generalize `IntoWand` for plainly/persistently.more unicodeadd a test for 'done' not to looptest iAssumption-based evar instantiationimprove core: don't use implicationgeneralize core to all BIsWIP: make core general for all BIsralf/coreralf/coreadd a test for TC resolution not happening too earlyapply -> refineralf/tc_control2ralf/tc_control2expand FIXMEtake some part of robberts patchralf/tc_controlralf/tc_controlStart improving control over type class search in proof mode tactics.little change to update mtac2's kind_of_termMerge branch 'gen_proofmode' of gitlab.mpi-sws.org:FP/iris-coq into gen_proofmodeMake sure as_valid_embed is not used when there is no embedding.fix benchmark exportsealing: Use primitive projection notation introduced in Coq mastertweak benchmark exporteravoiding reduction in of_exprUse MakeMonPredAd in ElimModal instances.update coq-speed export scriptAdd test case.Merge branch 'gen_proofmode' of gitlab.mpi-sws.org:FP/iris-coq into gen_proofmodedecapp for to_expr and of_val in of_exprSplit [FromAssumption] into three, depending on wheter the parameters are evars. This is to avoid loops in TC search.Merge branch 'robbert/big_rename' into 'gen_proofmode'Typo.Notations <absorb>, <affine> and <pers>.Notations <obj> and <subj>.Rename absolutely → objectively and relatively → subjectively.We usually fail faster to prove IntoPure than Absorbing/Affine.More Hint Modes.Add iStartProof in iAccu.