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.024Mar22212019161514131298765432128Feb27262524232221201918161514131298763231Jan2927252423222120191816131211107331Dec30292322212019181514131211108765432130Nov292827262423222120181615gitlab-extract: add support for excluding a branchupdate CIwe can't use variables in 'only:', so go back to OPAM_PKG_BRANCHupdate CI: use dedicated buildjob script, submit timing information to coq-speedCI needs submodules nowmove CI scripts to submoduleMerge remote-tracking branch 'origin/master' into gen_proofmodemore consistent lemma namingCI: test Coq 8.8 branchverified compatibility with Coq 8.8 (CI coming later)bump std++; no changes neededStop iFrame from introducing modalitiesmove Frame instances to their own filesplit class_instances into BI and SBI instancedsplit derived_laws into BI and SBI lawsmove general BI things using the proofmode down into lib/Merge branch 'ralf/intuitionistically' into 'gen_proofmode'apply Robbert's feedbackFromAffinely instance for intuitionistic modalityteach framing about the intuitionistic modalityadd tons of instances for the intuitionistic modalityget rid of 2nd into_persistent_intuitionistically instanceMerge branch 'ralf/valid' into 'gen_proofmode'update iIntoEmpValid docsiIntoValid -> iIntoEmpValidrename valid -> emp_validrename affinely_persistently -> intuitionistically; and make it a TC-opaque definitionFix typo.Merge branch 'gen_proofmode' of https://gitlab.mpi-sws.org/FP/iris-coq into gen_proofmodeWeaken BI axiom `P ⊢ <pers> emp` into `emp ⊢ <pers> emp`.rename env_persistent -> env_intuitionisticmake the README less outdatedfix 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.