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.011Jan109876543128Dec2625242322212019181716151413121198762130Nov29282726252423221615111098743128Oct272625166316Sep151413121110965226Aug241898421Jul1312118732130Jun272423solve_inG ftwrename soundness -> adequacyI can't make a commit with a new file without forgetting to add it...Merge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coqSoundness of the type system. Also, added a file typing.v that reexports all the type system.lang/heap: do sealing with primitive projectionsMake it possible to nest uninit products for subtyping.Alpha renaming.Have subtyping between product of uninit and uninit automatically proved.More uses of [iDestruct ty_size_eq].Forgot a file.Cleaning : remove hints about [product2] from solve_typing (this type is only for internal use), and removed unnecessary unfold lemmas.Merge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coqTypechecked lazy lifetime initialization. Also, switched from eauto to typeclasses eauto, which seems way less bugged (but I still found something strange...).use the fact that we can specialize lemmas below laterTypechecking unwrap_or.Merge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coqprove writing to Cell; tune some notationMerge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coqType-checking option_as_mut.forgot to add cell to _CoqProjecttyping/tests: make all the functions values as they should beProve that Cell<T> is a type and copy if T is copytry and fail to make using ty_size_eq on \later own more convenientawk.Makefile: uninstall .v and .glob filesawk.Makefile: uninstall: also delete empty directoriesfix awk.Makefilehide the lifetime logic CMRAs behind the signature as wellupdate awk.MakefileMerge commit '7726a27bb6ee6b89e1f4333bef098357ca0b8cf0'Trying to clarify priorities of mergeing and splitting lemmas. Clearly, this is still not optimal.Merge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coquse solve_inG tacticupdate IrisSimplify the proof of init_prod.Make the pattern for [tctx_extract_hasty_here_eq] more robust.New example : init_prod.I forgot to update _CoqProject.Merge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coqType unbox.