Skip to content
Snippets Groups Projects
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
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.015Mar1310976543128Feb25242322211918171615131211109830Jan262524232221191716131211109876543128Dec2625242322212019181716151413121198762130Nov29282726252423221615111098743128Oct272625166316Sep151413121110965226Aug241898421Jul1312118732130Jun272423Update to latest Iris.prove Rc::try_unwrapadd Rc::try_unwrap codeMerge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coqchange 'cont:' syntax to have explicit binderMake type_jump easier to use by not having to give it the list of parameters.Prove weakening lemmas for elctx_sat.note what is still missing for RcRc::get_mutmake it so that we can give the option type (instead of the list of variants) to the type_sum lemmasRc::drop*oops* undo accidental changesRc::drop codeMerge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coqRc::derefBump Iris and fix some minor things.Obligation Tactic is already idtac.Bump Iris.Use the new LimitPreserving stuff.Params instances for Copy, Sync, Send.Declare some Params instances to speed up rewrites.update to latest IrisRc::cloneintroduce notation for the magic return variable nameforce typed_val to be used only on valuesmask tweakingrc can be createdrc is still a type, but a more complicated onelater-P and static-borrow-of-P are view-shift equivalentadd typing.base; declare solve_typing and its DBs therefactor out the "delayed sharing" pattern used by own, uniq, refcell, rwlockFix buildfunction types: make FP the nice constructor and FP' the ugly oneMerge branch 'jh/alive_coercions' into 'master' Notation FP' as a wrapper for FP, so that the arguments are in the right order.Make the notation for function types work even if used with more than on variable.Make [ELCtx_Alive] a coercion.Make [lft] an Opaque type, when seen from outside of the lifetime logic model.Merge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coqrc is a type