Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
Select Git revision
  • ci/debug
  • ci/for_proph
  • ci/general-contractive
  • ci/hai/siProp
  • ci/janno/strict-tc-resolution
  • ci/msammler/nb_state
  • ci/ralf/Z_of_nat
  • ci/ralf/bi-language
  • ci/robbert/big_op_binder
  • ci/robbert/contractive_ne
  • ci/robbert/coq_bug_7773
  • ci/robbert/faster_iDestruct
  • ci/robbert/faster_iDestruct2
  • ci/robbert/faster_iFresh_joe
  • ci/robbert/frame_fractional
  • ci/robbert/iFrame
  • ci/robbert/into_fupd
  • ci/robbert/into_val_pures
  • ci/robbert/kill_locked_value_lambdas
  • ci/robbert/mapsto_persist
  • iris-4.0.0
  • iris-3.6.0
  • iris-3.5.0
  • iris-3.4.0
  • iris-3.3.0
  • iris-3.2.0
  • iris-3.1.0
  • iris-3.0.0
  • iris-2.0
  • iris-2.0-rc2
  • iris-2.0-rc1
  • iris-1.1
  • iris-1.0
  • hope-2015-coq-1
  • appendix-1.0.0
  • appendix-1
36 results
Created with Raphaël 2.2.021Feb2018171615141312111097632130Jan2928272625242322212017131211109876543128Dec2726232221201918161514131211987652130Nov2928272625242322212019181716151098765432131Oct30282726252221181716151413121097654fixpointK_indUpdate opam-ciuse new CI machineUnify tokenizers for intro, spec, and sel patterns.Fix typos.we totally did not record timing in artifacts since we switched to 8.6-only...Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqadd eauto hint Db for calling solve_ndisjGeneralize iso_cofe infrastructure to deal with types in lambdarust.Make solve_ndisj more powerful.Add an eauto test.Make (e)auto enter proofmode when we are not already in it.Add a missing iStartProof.fix arrowsfix namingfix types of the new instancesmore FromPure and IntoPure instancesMerge branch 'janno/into-pure-instances' into 'master' Add IntoPure instances for ∗, ∧, and ∨.Remove an Ltac hack that was there for unknown reason.Merge branch 'ralf/contrib' into 'master' Add a test for 9ea6fa45.Let iAssumption succeed when there is H : False.When using [iAssert ... with ">[]"], we should not use [tac_assert_persistent], and eliminate the modality instead.add a contributor's guideMake iSpecialize work with coercions.Better error message for iSpecialize.Improve `iSpecialize ("H" $! x1 .. xn)`.Improve `iIntros "_"`.Proper instances for types classes over ofe and cmra elements, and upreds.More currying in gen_heap.Merge branch 'swasey/invariance' into 'master' Make it possible to apply the observational view shift lemmas.Shorten OFE construction for vectors.More support for constucting isomorphic COFEs.Misc stuff about sigC.More constructors for LimitPreserving.Hint Mode for LimitPreserving.Bump Iris version.Easier way to construct OFEs that are isomorphic to an existing OFE.