Skip to content
Snippets Groups Projects
Select Git revision
  • ci/artifacts
  • ci/buildcache
  • ci/coqdoc
  • ci/debug
  • ci/opam2
  • ci/perf
  • ci/ralf/mangled
  • coq-stdpp-1.0
  • fix-export
  • instance-nobody-open-proof
  • master default protected
  • options
  • ralf/exact_vm_cast
  • ralf/notation
  • robbert/map_seq
  • robbert/set_rename
  • 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.01Feb29Jan28252419131119Dec16151412330Nov28262220121110984130Oct2917157430Sep181Aug23Jul171030Jun292825232120181410976530May2928242314927Apr242119181110965328Mar27222186123Feb22211916151312983231Jan25231413121019Dec181785429Nov282221201816121193131Oct2827242019181716131097629Sep28272624212019181786222Aug17825Jul26Jun30May251Apr20Mar171615141198123Feb221916151413109764331Jan9Dec86529Nov2423222120191817161510727Oct134328Sep27212014929Aug24221917842127Jul25232220121153130Jun26231814131May30292723429Apr1311730Mar292322211110543227Feb262524232221201917161514update 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 explicitinstance-nobody…instance-nobody-open-proofsilence fewer warnings, add comment about overwriting notationralf/notationralf/notationMerge branch 'robbert/bool_of_tc' into 'master'mastermaster`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`.Consistently use `set_` prefix.robbert/set_ren…robbert/set_renameShow that accessible elements do not loop.`set_seq` is finite.robbert/map_seqrobbert/map_seqRelation between `set_seq` and `seq`.Support `set_seq` in `set_solver`.Relation between `map_seq` and `set_seq`.Make `set_seq` lemmas for consistent w.r.t. those of maps.Rename `seq_set` into `set_seq` to be consistent with `map_seq`.Function `map_seq` to turn a list into a finite map of consequentive elements.