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.01May30Apr29282728272623222120212019201918171413876532131Mar30292824181716151110989763212128Feb1Mar28Feb27231816141211830Jan292625421Dec1610326Nov21171311531Oct3029221913109532130Sep29281587653226Aug23Jul22151098763230Jun191229May24158724Apr23874231Mar302120181613121193226Feb25242119181715141312117419Jan18131117Dec13109322Nov21128731Oct2221109875425Sep23201918171513116543231Aug302928272625231613129643131Jul3029262524232217small fixremove applicative and reader monadrevert names for lifetime intersectionsmall fixshorter names for lifetime intersectionProve sharing of unique borrowsinline type_memcpy_irisfix notation for fnrecprove type_fnrec_instr and type_fn_instradd a comment about Hint Extern for subtypel/eqtypelprove fn_subtype and fn_subtype_specializeStore lifetime inclusion in unique borrowswipprove fn_type_contrfix proofprove fn_nemodel the function typesplit arguments of val_obs and proph_ctrlfix prooffix CI configdon't test against Coq master (it is broken)don't test against Coq master (it is broken)don't test against Coq master (it is broken)fix proofFixes from rebaseProve unnesting a borrow of a box into a borrowfinish cont.veliminate tlistparametrize semantic types by syn_typefix prooffix proofdecidable inhabitedness for syn_typefix type syntax for the prophecy libraryintroduce syntactic Coq typeProve borrowingProve read_uniq and write_uniqgeneralize util/types.v to use any type rather than just Type, renaming it to util/fancy_lists.vfix proofuse Frakturs for TYPEEqDecision in prophG/prophPreG