Skip to content
Snippets Groups Projects
Select Git revision
  • atomic
  • ci/janno/vmcast
  • ci/ralf/atomic
  • ci/ralf/lia
  • ci/ralf/pm_red
  • ci/ralf/telescopes
  • fast_string
  • gen_proofmode
  • iris-3.0
  • iris-3.1
  • janno/metacoq
  • jh/done_contradiction
  • jh/evar_iframe
  • jh/independent_metric
  • jh/sprop_upred
  • jh_inductive_pairs
  • joe/defined_pers
  • less_canonical
  • less_canonical_new
  • marianna/prophecy
  • 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.05Mar432129Feb28272625242322212019181716151413121110985432introduce "fast_done", a tactic that *quickly* tries to solve the goalMakefile attributiontry to speed up set_solver a littleimprove Makefile: fix make dir/name.vounify the two invariants of the barrier protocol, this drastically simplifies recv_splitchange wp notationignore more logfilessome more commentsExpressions as dependent type.List inclusion in terms of list membership.Let set_solver handle some list connectives.simplify_eq now handles existT if the indexing type is decidable.fix gitlab extractor to be more robustSeal off definition of iProp using a Module.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqMove closed stuff to lang and prove some properties about it.Hint database for set_solver.New destruct_and tactic that also deals with Boolean ands.run CI job only for master branchMake naive_solver deal with some Boolean connectives.better position for the legendMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqbenchmak/visualizer: can now restrict the graph to a given commit rangeMore consistent names for scopes in heap_lang.Rename values_stuck -> val_stuckMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqnotation for locationsrename BAnom -> BAnon; avoid overloading notation in the same scopeTweak functor for function spaces.test for 'crazy higher order'define functor for function spaceget rid of substitution in Case (use lambdas); introduce Match as derived form that involves bindersClean up anonymous binder hack.Use notation # instead of ' for literals to avoid conflicts.Generalize saved_props to any bifunctor.demonstrate a weird issueralf/magic-sing…ralf/magic-singletonWIP: nicer definition of head_stepMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqIntroduce cofeT -> cofeT functors, switch to bifunctors.WIP: expr as dependent type