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.014Mar131298765432128Feb27262524232221201918161514131298763231Jan2927252423222120191816131211107331Dec30292322212019181514131211108765432130Nov292827262423222120181615141312119fix 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 somethingCoq future-compat: use qualified name foriFresh: Force start proof when iFresh is called.Store a counter in to assign fresh names with .Add hint for introducing absorbingly.Prove `<absorb> □ P ⊣⊢ <pers> P` and use it to refactor some stuff.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 BIsadd a test for TC resolution not happening too earlyexpand FIXMEStart improving control over type class search in proof mode tactics.Merge 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 exporterUse 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_proofmodeSplit [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'