Skip to content
Snippets Groups Projects
Select Git revision
  • coq-stdpp-1.0
  • master default protected
  • mraise
  • coq-stdpp-1.8.0
  • coq-stdpp-1.7.0
  • 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
13 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.029Oct2821201513762129Sep161583231Aug3028724Jul2117161514102129Jun2523191817151429May2827261276130Apr292320171615111098765432131Mar302519181713109528Feb2625242320191817141311130Jan181716151319Dec622Nov2111762131Oct7119Sep1211529Aug27262423151413713Jul98754330Jun2827262521201814230May26252117151210984330Apr2625241926Mar161514643128Feb2322212017131076129Jan28252419131119Dec1615141230Nov28262220121110984115Oct7430Sep181Aug23Jul171030Jun292825232120181410976530May2928242314927Apr2421181110965328Mar2722218623Feb2221Rename `Qp_eq` into `Qp_to_Qc_inj_iff`.Extend the theory of the positive rationals `Qp`.Remove space.reduce TC assumptions made by fin_to_setmore old Coq failuresfix build on old Coqfix buildMerge branch 'ralf/fin_to_set' into 'master'add SetUnfoldElemOf instanceOops.Merge branch 'ralf/dom_insert_lookup' into 'master'Apply 1 suggestion(s) to 1 file(s)Merge branch 'robbert/cleanup' into 'master'CHANGELOG.Remove dead type classes and notations.add a way to obtain a set with all elements of a finite typeadd dom_insert_lookupMerge branch 'add-union-fmap' into 'master'Add map_fmap_union for FinMapMerge branch 'robbert/implicit_names' into 'master'Avoid relying on implicit instance generalization, and name some instances.Merge branch 'ci/ralf/drop-8.9' into 'master'fix typo in MakefileMerge branch 'ci/ralf/makefile' into 'master'remove now-redundant package name from opam fileupdate build systemdeclare scopes before using themdrop support for Coq 8.8 and 8.9Merge branch 'qp-lemmas' into 'master'Remove Qp_not_plus_q_ge_1Change eapply to applyAdd Qp lemmasAdd `Countable` instance for `fin`.Merge branch 'ralf/lower-bound-lt' into 'master'add version of Qp_lower_bound that returns less-than factsAdd lemma `omap_insert_None`.update CI configDefault Goal Selector does not work that way on Coq 8.8Merge branch 'ralf/options' into 'master'fix base.v import order; use real import in prelude.v