Skip to content
Snippets Groups Projects
Select Git revision
  • ci/janno/reduction_no_check
  • ci/places
  • ci/pm_red
  • ci/ralf/const-rf
  • ci/ralf/lia-experiment
  • ci/ralf/old-timing-data
  • ci/ralf/sections
  • ci/robbert/faster_iDestruct2
  • ci/robbert/iprop_structures
  • ci/robbert/merge_sbi
  • ci/robbert/merge_sbi_new
  • ci/robbert/merge_sbi_new_weak
  • ci/robbert/merge_sbi_weak
  • ci/robbert/naive_solver
  • ci/weak_mem
  • contractiveness
  • coqbug/match
  • fast_string
  • ghostcell
  • gpirlea/pinning
  • RBrlx-POPL20-artifact
  • popl18
  • popl18-aec
23 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.06Oct5428Sep272625212019729Aug28242221191716108432131Jul19171611107643220Jun18May171615131294229Apr282726252422201918141311730Mar28272423222116151310976543128Feb25242322211918171615131211109830Jan262524232221191716131211109876543128Dec2625242322212019181716151413121198762130Nov2928272625remove empty modules filesstop excluding files from git exportsavoid newline in quoted textpopl18-aecpopl18-aecexplain updatingexpand READMEmove sharing lemmas around so that uniq does not depend on shrREADME: mention minimal opam versionREADME: mention -jMerge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coqfix build-dep/opam dependenciesMerge remote-tracking branch 'origin/eq-loc'support MacOSrename CI jobsstrengthen qp_eq_loc; add a testwp_eq_loc: don't throw away the mapstosMerge remote-tracking branch 'origin/master' into eq-locdocument pointer comparison non-determinismupdate awk.Makefileupdate Irisupdate for Coq Makefile hooksupdate Makefile, gitignoreupdate Irisupdate build systemupdate READMEcoqchk is brokenRemove workaround.update Iris; get rid of opam.pinsAdding iris atomicMerge branch 'master' of mpisws-gitlab:FP/lambdarust-coqAdding location equality.It is not necessary to ask lifetime inclusion to trade dead tokens.jh/lifetime_no_…jh/lifetime_no_dead_tradeadd missing fileshow that we can covnert 'a to 'static if the function never returnsIdem for the types of shared and unique borrows.Change the notation for borrows : now, it is just a notation for the predicate transformer (it does not include the payload of the borrow).no longer test Coq 8.6; start testing 8.7update Irisupdate CI to templates; test against 8.6.1Simplify proofsThe inheritance of raw reborrowing is not (no longer) necessary. Let's remove it and call it shorten.