Skip to content
Snippets Groups Projects
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
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.016Mar151413121198765432128Feb27262524232221201918161514131298763231Jan302927252423222120191816131211107331Dec30292322212019181514131211108765432130Nov292827262423Weaken BI axiom `P ⊢ <pers> emp` into `emp ⊢ <pers> emp`.rename env_persistent -> env_intuitionisticAdd error reporting to `iStartHeapProof`.Make `iStartHeapProof` slow but beautiful.Add and use CPS `reshape_val_dep`.make the README less outdatedAdd certified `reshape_val` and `reshape_expr`.Remove scope annotations.fix a fluketypono idea why I would think this implies monotonicity...pers-emp actually just needs `core ε = ε`Merge branch 'gen_proofmode' of https://gitlab.mpi-sws.org/FP/iris-coq into gen_proofmodeshow that persistently is also another fixpointMerge branch 'joe/fresh' into 'gen_proofmode'Reorganize monpred.v and no longer upclose bupd and fupd.iFresh: document the Ltac trick to force evaluation of the side-effect.note that forall_2 would be derivable in a classical meta-logicshow that persistently and affinely-persistently are fixpoints of somethingAdd a backtracking exception to reshape_expr_M.Add error message to `iStartHeapProof`.Some cleanup in tactics/proofmode.v.Move `iStartProof` to proofmode/tactics.v.Make exc'n logic of `reshape_expr_M` consistent.Coq future-compat: use qualified name foriFresh: Force start proof when iFresh is called.Store a counter in to assign fresh names with .Add error reporting to `wp_pure`.Use `TT.apply`, `TT.apply_`.Use `TT.apply` in `wp_value_head`.Add hint for introducing absorbingly.beautified iStartProof (in proofmode/tactics)Prove `<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.