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.09Mar76543128Feb25242322211918171615131211109830Jan262524232221191716131211109876543128Dec2625242322212019181716151413121198762130Nov29282726252423221615111098743128Oct272625166316Sep151413121110965226Aug241898421Jul1312118732130Jun272423Bump 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 typeMerge branch 'jh/undiscriminated_hintdb'Merge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coqMove non-core typings into theories/typing/libTry making [lrust_typing] non-discriminated to see whether anything changes.Tweak.Merge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coqFaking a shared box.Make solve_typing able to solve [typed_read] and [typed_write].lrust_typing: make sum type opaque, for consistency with the other typesfix comment in spawn.vMerge branch 'ralf/ci/box' into 'master' Fix [solve__typing] by changing the hint on [tctx_extract_hasty_here_eq] into a [Hint Resolve], so that the opaqueness annotations are not ignored.Make box a definition and prove it contractiveNew notation : typed_val.bump Irisswitch to new CI machineforgot to bump Iris