Skip to content
Snippets Groups Projects
Select Git revision
  • ci/artifacts
  • ci/buildcache
  • ci/coqdoc
  • ci/debug
  • ci/opam2
  • ci/perf
  • ci/ralf/mangled
  • coq-stdpp-1.0
  • fix-export
  • instance-nobody-open-proof
  • master default protected
  • options
  • ralf/exact_vm_cast
  • ralf/notation
  • robbert/map_seq
  • robbert/set_rename
  • coq-stdpp-1.1.0
  • coq-stdpp-1.0.0
18 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.025Jun232120181410976530May2928242314927Apr242119181110965328Mar27222186123Feb22211916151312983231Jan25231413121019Dec181785429Nov282221201816121193131Oct2827242019181716131097629Sep28272624212019181786222Aug17825Jul26Jun30May251Apr20Mar171615141198123Feb221916151413109764331Jan9Dec86529Nov2423222120191817161510727Oct134328Sep27212014929Aug24221917842127Jul25232220121153130Jun26231814131May30292723429Apr1311730Mar292322211110543227Feb2625242322212019171615141311109842127Jan222018161412422Dec2115118420Nov19181716113Feb110Jun5221May22Apr1615Mar225Feb2416138130Jan29272523Dec1816Merge branch 'ralf/rtc' into 'master'add .gitattributes for GitLab syntax highlightingdecrease priority for rtc_reflexive instanceupdate CIupdate CI to use perfrerun CIci/perfci/perftry putting time inside perfrerun CIupdate CI to use perfjust fill the build cachesci/buildcacheci/buildcacheMerge branch 'ralf/lia' into 'master'also time Coq 8.8use lia instead of omegaMerge branch 'ralf/difference_union' into 'master'add lemma about chained differencegeneralize ndisj_subseteq_difference to work for all masksMerge branch 'ralf/solve_ndisj' into 'master'solve_ndisj: try harderMisc result about Qp.add format specifier tp single-symbol notationMerge branch 'ralf/telescopes' into 'master'Teach typeclass resolution to make progress on telescopic bindersFix universe inconsistency in Iris by making telescopes universe polymorphicadd telescopic versions of the Coq quantifiersrename lemmas about telescope function space to tele_fun_*Merge branch 'ralf/telescopes' into 'master'also provide a composition for the function spaceshow that tele_app ∘ tele_bind is an identity; remove unused strange fmap instanceadd telescopes and a bit of theory about them.gitignoreupdate CI and MakefileMerge branch 'ralf/default' into 'master'coqdocintroduce [default] as abbreviation for [from_option id], and use itMerge branch 'ralf/default' into 'master'Remove the `default` notation for optionsMisc results about `Qp` fractions.Literals 2, 3, and 4 for `Qp`.Prove `m ∖ m = ∅` for finite maps.update CI/Makefile