Skip to content
Snippets Groups Projects
Select Git revision
  • coq-stdpp-1.0
  • glen/finite-nodec
  • master default protected
  • msammler/bitvector
  • msammler/bool_decide_simpl_never
  • ralf/hint-mode-check
  • robbert/cbn
  • robbert/f_equiv_pointwise
  • robbert/from_option
  • robbert/map_filter_True_False
  • robbert/multiset_singleton
  • robbert/tc_opaque
  • tchajed/stdpp-sprop-gmap
  • coq-stdpp-1.6.0
  • coq-stdpp-1.5.0
  • 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
21 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.031Jan9Dec86529Nov2423222120191817161510727Oct134328Sep27212014929Aug24221917842127Jul25232220121153130Jun26231814131May30292723429Apr1311730Mar292322211110543227Feb2625242322212019171615141311109842127Jan222018161412422Dec2115118420Nov19181716113Feb110Jun5221May22Apr1615Mar225Feb2416138130Jan29272523Dec181623Nov1569Oct86230Sep251613126326Aug22976410Jul425Jun23171676524May22429Sep27Aug2115141224Jun1721May15121172Apr25Mar1424Feb221919Jan512Nov19Oct104Sep30Aug29242121Jun1411Bump year in prelude copyright headers.Vector tweaks.Use primitive projections for sealingMake instances EqDecision and Countable of gmultiset less eager.Recursive [inv_vec].Renaming in prelude/list.more restrictive Proof Using hints in (most files of the) preludeTweak some proof using tweaks for setoid stuff.tune "Proof using" directives to minimize differences to previous types of all lemmasdon't use Proof Using in a few files that get too many unnecessary annotations from thisRequire `Total R` just for the merge sort theorems that actually need it.Document list_remove and list_remove_list.Fix more _L lemmas.make "make quick" quick by adding hints about the used section variablesadd decide_left, decide_rightMove stuff out of sections that does not depend on the section variables.Simplify proofs relating nth to lookup.list: relate nth and lookupA few lemmas about vec and fin.Rename fmap_Some_equiv' → fmap_Some_equiv_1.rename _setoid suffix to _equiv; add variant of fmap_Some_setoid that can be usefully destructedFix breaking ee6df099.Optimize simplify_eq.Avoid exponential blowup in [done] as caused by a7e91677.fix compatibility with latest Coq 8.6Factor out some common properties about lists.New definition of contractive.Some more of_list stuff.More multiset stuff.Fix typo.Merge branch 'nclose_subseteq' into 'master' Some tweaks to minimal.Make some arguments explicit that could not be infered.More set_Forall and set_Exists stuff for finite sets.Make nclose an explicit coercion.Comment on commit 44cfd7d3.Patch naive_solver to deal with Coq bug #2901.Function to convert a multiset into a gset.prove fmap_Some_setoidmake done and fast_done more consistent in behavior