Skip to content
Snippets Groups Projects
Select Git revision
  • ci-release protected
  • ci/msammler/more_feed
  • ci/refactor_staging
  • coq-stdpp-1.0 protected
  • dfrumin/coq-stdpp-set_map_2
  • master default protected
  • msammler/bitvector
  • msammler/bool_decide_simpl_never
  • msammler/monad_without_universe_constraints
  • ralf/empty-opaque
  • ralf/hint-mode-check
  • ralf/hint-mode-plus
  • ralf/list-module
  • ralf/listZ
  • ralf/lookup_insert
  • ralf/make_simple_intropattern
  • ralf/multiset-solver
  • robbert/cancel_inj_surj
  • robbert/cbn
  • robbert/f_equiv_pointwise
  • coq-stdpp-1.11.0 protected
  • coq-stdpp-1.10.0 protected
  • coq-stdpp-1.9.0 protected
  • coq-stdpp-1.8.0 protected
  • coq-stdpp-1.7.0 protected
  • coq-stdpp-1.6.0 protected
  • coq-stdpp-1.5.0 protected
  • coq-stdpp-1.4.0 protected
  • coq-stdpp-1.3.0 protected
  • coq-stdpp-1.2.1 protected
  • coq-stdpp-1.2.0 protected
  • coq-stdpp-1.1.0 protected
  • coq-stdpp-1.0.0 protected
33 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.020Feb17131076129Jan28252419131119Dec1615141230Nov28262220121110984115Oct7430Sep181Aug23Jul171030Jun292825232120181410976530May2928242314927Apr2421181110965328Mar2722218623Feb22211916151312983231Jan25231413121019Dec181785429Nov282221201816121193131Oct2827242019181716131097629Sep28272624212019181786222Aug17825Jul26Jun30May251Apr20Mar171615141198123Feb221916151413109764331Jan9Dec86529Nov2423222120191817161510727Oct134328Sep27212014929Aug24221917842127Jul25232220121153130Jun26231814131May30292723429Apr1311730Mar292322211110543227Feb26252423222120191716tweak proofsAlternative versions of finite/infinite predicates in terms of sets.Add a notion of finite/infinite predicates and define finite/infinite sets using it.Support `elements` in `set_solver`.CHANGELOG 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.