Skip to content
Snippets Groups Projects
Select Git revision
  • coq-stdpp-1.0
  • master default protected
  • ralf/options
  • robbert/cbn
  • robbert/from_option
  • robbert/tc_opaque
  • 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
12 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.06Feb129Jan28252419131119Dec1615141230Nov28262220121110984115Oct7430Sep181Aug23Jul171030Jun292825232120181410976530May2928242314927Apr2421181110965328Mar2722218623Feb22211916151312983231Jan25231413121019Dec181785429Nov282221201816121193131Oct2827242019181716131097629Sep28272624212019181786222Aug17825Jul26Jun30May251Apr20Mar171615141198123Feb221916151413109764331Jan9Dec86529Nov2423222120191817161510727Oct134328Sep27212014929Aug24221917842127Jul25232220121153130Jun26231814131May30292723429Apr1311730Mar292322211110543227Feb2625242322212019171615141311109842127Jan22201816Clean up imports in `infinite` file.found some more URLs to updateupdate opam repo URLupdate more URLsupdate URLfix or silence Coq 8.10 warningsMake rtc an instance of PreOrder.Better use of unicode in type classes test file.Update years in copyright headers.More consistency in relations.v.Fix typo.Merge branch 'ralf/notation' into 'master'test against Coq 8.9.0More documentation for solve_proper_prepare + introduce more.update MakefileCOQTEST: get rid of old filtering stufftweak COQTEST outputuse egrep -qMerge branch 'ralf/tele' into 'master'put notation into stdpp_scopefix λ.. printing and test itMerge branch 'master' of https://gitlab.mpi-sws.org/iris/stdppfix print spacing of telescopesdo not override notationMerge branch 'instance-nobody-open-proof' into 'master'Make trivial instances explicitsilence fewer warnings, add comment about overwriting notationMerge branch 'robbert/bool_of_tc' into 'master'`tc_to_bool P` to turn a type class into a Boolean that represents if there is an instance.update CI configMerge branch 'map_filter_lemmata' into 'master'Add results about deleting and inserting filtered out elementsMerge branch 'master' into 'master'Get rid of the awk.Makefile referencesInline equality premise in `map_insert_zip_with`.Show that accessible elements do not loop.Bit of clean up.Type class version of `elem_of` for lists.Merge branch 'add_docs_to_readme' into 'master'Merge branch 'no-implicit-core' into 'master'