Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
Select Git revision
  • ci/ike/frame_exist
  • ci/janno/reduction_no_check
  • ci/janno/strict-tc-resolution
  • ci/pinning
  • ci/places
  • ci/pm_red
  • ci/ralf/const-rf
  • ci/ralf/sections
  • ci/weak_mem protected
  • coqbug/match
  • ghostcell
  • gpirlea/pin_semantic
  • gpirlea/pinning
  • jh/closures
  • jh/dynamic_masks
  • jh/lifetime_no_dead_trade
  • jh/typecheck_foo
  • master default protected
  • masters/rusthornbelt protected
  • masters/weak_mem protected
  • RBrlx-POPL20-artifact
  • popl18
  • popl18-aec
23 results
Created with Raphaël 2.2.010May987656543130Apr29282728272623222120212019201918171413876532131Mar30292824181716151110989763212128Feb1Mar28Feb27231816141211830Jan292625421Dec1610326Nov21171311531Oct3029221913109532130Sep29281587653226Aug23Jul22151098763230Jun191229May24158724Apr23874231Mar302120181613121193226Feb25242119181715141312117419Jan18131117Dec13109322Nov21128731Oct2221109875425Sep23201918171513116543231Aug302928272625231613129643131Jul30Merge remote-tracking branch 'origin/master' into masters/weak_memsmall fixsmall fixprove various leak rules; update forall definitionsprove more leak rulesfix the model of Leakmodify tctx_uniq_mod_ty_outsmall fixUpdate dependencyprove tctx_extract_merge_own/shr_xprodMerge branch 'jh/fn_notation' into 'master'prove tctx_split_uniq_xprodprove tctx_split_uniq_prodfix proofsintroduce Leak and prove uniq_leakUpdate dependenciessmall fixProve reborrowingupdate dependenciesupdate dependenciessmall fixswap arguments of tctx_incl_impl/eqprove product split/merger for own_ty and shr_borThe introduction pattern \!# is deprecated. Replace by \!>.Improve notations for functionsuse nth for the sum typefix basic proofsFinish borrow.vProve statement version of unnestingProve some minor lemmas about borrowingProve deref-own-shrProve unnesting of unique referencesadd frame instancesNit.prove type_call and type_letcallsmall fixremove applicative and reader monadrevert names for lifetime intersectionsmall fixshorter names for lifetime intersection