Skip to content
Snippets Groups Projects
Select Git revision
  • coq-stdpp-1.0
  • glen/finite-nodec
  • master default protected
  • msammler/bitvector
  • msammler/bool_decide_simpl_never
  • ralf/hint-mode-check
  • robbert/cbn
  • robbert/f_equiv_pointwise
  • robbert/from_option
  • robbert/map_filter_True_False
  • robbert/multiset_singleton
  • robbert/tc_opaque
  • tchajed/stdpp-sprop-gmap
  • coq-stdpp-1.6.0
  • coq-stdpp-1.5.0
  • coq-stdpp-1.4.0
  • coq-stdpp-1.3.0
  • coq-stdpp-1.2.1
  • coq-stdpp-1.2.0
  • coq-stdpp-1.1.0
  • coq-stdpp-1.0.0
21 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.018Jun1410976530May2928242314927Apr2421181110965328Mar2722218623Feb22211916151312983231Jan25231413121019Dec181785429Nov282221201816121193131Oct2827242019181716131097629Sep28272624212019181786222Aug17825Jul26Jun30May251Apr20Mar171615141198123Feb221916151413109764331Jan9Dec86529Nov2423222120191817161510727Oct134328Sep27212014929Aug24221917842127Jul25232220121153130Jun26231814131May30292723429Apr1311730Mar292322211110543227Feb2625242322212019171615141311109842127Jan222018161412422Dec2115118420Nov19181716113Feb110Jun5221May22Apr1615Mar225Feb2416138130Jan29272523Dec181623Nov1569Oct86230Sep2516131263generalize 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/MakefileSome forgotten occurences of only parsing.Get rid of fix/cofix without a name; these are deprecated in Coq 8.8.update CIsolve_proper_unfold: support functions with more argumentsf_equiv: recognize 2-level pointwise_relationupdate CIre-publish opam packagetest against Coq 8.8.0; update CI`Equivalence` for `≡` on gmultisets.Merge branch 'master' into 'master'`Equiv` instance for multisets.Consistent and higher precedence for default [Equiv] instances on maps/collections.Merge branch 'robbert/rel_disambig' into 'master'Notation `≡ₚ@{A}`.Notation `⊑@{A}`.