Skip to content
Snippets Groups Projects
Select Git revision
  • atomic
  • ci/3.1.0
  • ci/debug
  • ci/janno/debug-opam
  • ci/janno/vmcast
  • ci/ralf/ci
  • ci/ralf/pm_red
  • ci/robbert/into_val_pures
  • ci/stability
  • ci/value_constructor
  • fast_string
  • iris-3.0
  • iris-3.1
  • janno/metacoq
  • jh/done_contradiction
  • jh/evar_iframe
  • jh/independent_metric
  • jh/sprop_upred
  • jh_inductive_pairs
  • joe/bupd_derived
  • 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
30 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.020Feb181716151413121110987632130Jan2928272625242322212017131211109876543128Dec272623222120191817161514131211987652130Nov2928272625242322212019181716151098765432131Oct302827262522211817161514131210976Update 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.Trigger CI.jh/done_contrad…jh/done_contradictionMake iAssumption use timelessness is possible.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.