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.09Apr654331Mar28272422212019161514131298765432128Feb27262524232221201918161514131298763231Jan2927252423222120191816131211107331Dec30292322212019181514131211108765432130Nov2928272624only run coqchk in one jobbump std++rename : affinely_persistently -> intuitionistically. Add lemma about monpred_at and intuitionistically.ofe_funC_ofe_discrete and ofe_funR_cmra_discrete.update CImove OPAM_PKG to the 8.8+beta1 job as that one is spawned firstalso time against Coq 8.8 betaupdate std++ to make sure we have all notations aroundMerge branch 'ralf/bi_disambig' into 'gen_proofmode'fix notation conflictmake the annotated notations only parsing; add annotated versions of the curried forms (⊢) and (⊣⊢)add '@' to type ascription notation for disambiguationadd notation to define the PROP we use for a particular turnstileMerge branch 'robbert/ElimModal' into 'gen_proofmode'Separate type class for `■ ⎡P⎤ ⊢ ⎡■ P⎤`.Remove embed emp axiom.Document `ElimModal`.Extend ElimModal with Boolean flags to specify whether it operates on the persistent/spatial context.Merge branch 'gen_proofmode' of gitlab.mpi-sws.org:FP/iris-coq into gen_proofmodeMerge branch 'master' into gen_proofmodeupdate CIFix some bad names.Slightly more easy to use version of strong `inv_open`.Stronger version of `inv_open` that allows to close invariants in a different order.update CIMerge branch 'ralf/lemma_rename' into 'gen_proofmode'fix gitlab-extract output if build is still runningupdate CIstop adding the quick2vo targetupdate CIFix typos.Short proof of `big_sepL_delete`.update CIMerge remote-tracking branch 'origin/master' into gen_proofmodeupdate CIupdate CI: use centralized CI repo; submiting timing to coq-speedgitlab-extract: show which commit the bad line was inupdate CIupdate CIgitlab-extract: add support for excluding a branch