Skip to content
Snippets Groups Projects
Select Git revision
  • ci/ralf/debug
  • coq-stdpp-1.0
  • master default protected
  • msammler/list
  • msammler/naive_solver0
  • msammler/rotate
  • msammler/strings_in_prelude
  • options
  • ralf/reflexive
  • robbert/countable_list
  • robbert/list_find
  • robbert/set_unfold
  • robbert/tc_opaque
  • 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
18 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.020Sep19181786222Aug17825Jul26Jun30May251Apr20Mar171615141198123Feb221916151413109764331Jan9Dec86529Nov2423222120191817161510727Oct134328Sep27212014929Aug24221917842127Jul25232220121153130Jun26231814131May30292723429Apr1311730Mar292322211110543227Feb2625242322212019171615141311109842127Jan222018161412422Dec2115118420Nov19181716113Feb110Jun5221May22Apr1615Mar225Feb2416138130Jan29272523Dec181623Nov1569Oct86230Sep251613126326Aug22976410Jul425Jun23171676524May22429Sep27Aug2115141224Jun1721May15121172Apr25Mar1424Feb221919Jan512Nov19Oct104Sep30Aug29242121Jun1411remove version field from opam fileno more opam.pinsUpdate for Coq 8.7 coq_makefileAdd uncurry3 and uncurry4.Version of inj_countable with a total function.Get rid of type class instance finite_countable.Prove that generic trees are countable.restrict publishing to master branchtrigger opam-update repo after successful CI builddon't claim to be compatible with arbitrary dev version of Coqupdate opam file to reflect that we requrie Coq 8.6 nowadd opam descrNo longer test master using Coq 8.5pl3.Set Hint Mode for all classes in `base.v`.Make uses of Arguments more rubust.Put the inequality of delete_singleton_ne in the same direction as other _ne lemmas.Put delete_singleton lemmas together.Merge branch 'difference_lemmas' into 'master'Add some useful lemmas about `difference` and `delete`More TCForall lemmas.More documentation for the type class logical operators.Also add a type class version of Forall.Put the type class logical connectives in Prop.Prefix logical operators on the type class level with TC.adapt regexp for coq 8.7update opam file to express that we support 8.7also run CI against 8.7 branch (will switch to release once that happened)CI: use template; test 8.5.3, 8.6 and 8.6.1Use simple apply in f_equiv and solve_proper.Also type classes for conjunction and unit.Add Or type class.Merge branch 'haidang/coq-stdpp-hai/QpCountable'Some tweaks to Hai's commit.add countability for Q, Qc, and QpTweaks.Merge branch 'dfrumin/coq-stdpp-map_properties'Fix some spacing.Some map_zip/map_zip_with properties.Compatibility with Coq 8.5.A zip_with operation on finite maps.