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.06Mar3212128Feb1Mar28Feb27231816141211830Jan292625421Dec1610326Nov21171311531Oct3029221913109532130Sep29281587653226Aug23Jul22151098763230Jun191229May24158724Apr23874231Mar302120181613121193226Feb25242119181715141312117419Jan18131117Dec13109322Nov21128731Oct2221109875425Sep23201918171513116543231Aug302928272625231613129643131Jul302926252423221711928Jun2620181311105429May2625241615141312225Apr24314Mar127642128Feb2726222120151211754131Jan3024231587219Dec141021Nov161514874129Oct252420198765430Sep2120191813107653225Aug24222019829Jul2823update dependenciesupdate dependenciesuse coq 8.13.0 instead of 8.12.0 in .gitlab-ci.ymlmodify proof of proph_dep_constr2 to avoid a new featureupdate .gitlab-ci.yml to use step_indexing_controlled_by_ghosts of coq-irisuse iFrame and $ moreadd proph_tok_appadd proph_obs_properintroduce point-free notation for proph_obsmodify README.md to recommend using opam pinmodify step-taking update in ty_own_proph and ty_shr_prophadd own.v to _CoqProjectMerge branch 'rusthornbelt-box-type' into 'rusthornbelt'prove model for own_ptrlftN instead of lftEremove Let P in section ofe in type.vfinish section type_utilfinish section subtyping in type.vfinish section type (for traits) in type.vfinish section type_contractive in type.vfinish section ofe in type.vadd st_size to simple_typeput back wrongly removed code in type.vremove a commentfinish simple typemodify proofadd basic lemmas about typenew definition of typemake hints globalintroduce pval_depthless notationfix notation levelfix proofadd uniq camerafix proofCI timing jobci/janno/strict…ci/janno/strict-tc-resolutionsmall fix of proofmodify typeG and type_preG component namesmodify order about lang in _CoqProjectadd typing/type.v to _CoqProject