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.020Feb17131076129Jan28252419131119Dec16151412330Nov28262220121110984130Oct2917157430Sep181Aug23Jul171030Jun292825232120181410976530May2928242314927Apr242119181110965328Mar27222186123Feb22211916151312983231Jan25231413121019Dec181785429Nov282221201816121193131Oct2827242019181716131097629Sep28272624212019181786222Aug17825Jul26Jun30May251Apr20Mar171615141198123Feb221916151413109764331Jan9Dec86529Nov2423222120191817161510727Oct134328Sep27212014929Aug24221917842127Jul25232220121153130Jun26231814131May30292723429Apr1311730Mar292322211110543227Feb262524232221CHANGELOG entry about the big set/map rename.Merge branch 'robbert/map_seq' into 'master'`set_seq` is finite.Relation 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.Function `map_seq` to turn a list into a finite map of consequentive elements.Merge branch 'robbert/set_rename' into 'master'Comment about `Set_`.Rename `of_bools`/`to_bools` into `bools_to_natset`/`natset_to_bools`.Better names for convertion functions from `gset` and `coPset`.Consistently use `set` and `map` names.∈ on `listset` is decidable.explain NoDup_enumupdate MakefileMerge branch 'robbert/relations' into 'master'The different notions of confluence and properties about them.The symmetric and reflexive/transitive/symmetric closure.Remove `ars` hint database.Merge branch 'robbert/seal_fresh_generic' into 'master'Seal `fresh_generic`.Prove `map_zip_with_singleton`.Infinite instances for prod/sum.More generic `Fresh` instance for `gset`.More consistent indentation in `infinite`.Clean 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.