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.06Sep222Aug17825Jul26Jun30May251Apr20Mar171615141198123Feb221916151413109764331Jan9Dec86529Nov2423222120191817161510727Oct134328Sep27212014929Aug24221917842127Jul25232220121153130Jun26231814131May30292723429Apr1311730Mar292322211110543227Feb2625242322212019171615141311109842127Jan222018161412422Dec2115118420Nov19181716113Feb110Jun5221May22Apr1615Mar225Feb2416138130Jan29272523Dec181623Nov1569Oct86230Sep251613126326Aug22976410Jul425Jun23171676524May22429Sep27Aug2115141224Jun1721May15121172Apr25Mar1424Feb221919Jan512Nov19Oct104Sep30Aug29242121Jun1411Merge 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.Version of map_fold_insert for Leibniz equality.Stronger version of map_fold_insert.Prove that a permutation on lists corresponds to an injection between the keys.More properties about the order on finite maps.Let set_solver/set_unfold only touch Prop hyps.Redefine imap and imap2.relate Forall2 and ForallFix Coq 8.5 build.Tweak some proofs.Show equivalence of re-defined List.In and List.NoDup with Coq stdlib versionsConversion from ascii to nat.Prove empty_subseteq.Some missing copyright headers.Remove my name from the copyright headers.Move Fin theory from vector.v to fin.v; improve inv_fin to match what inv_vec can doMerge branch 'master' of https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdppimprove inv_vec to force the length of the vector