Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
Select Git revision
  • ci-release
  • ci/msammler/_1_2_lemmas
  • ci/msammler/more_feed
  • coq-stdpp-1.0
  • dfrumin/coq-stdpp-set_map_2
  • master default protected
  • msammler/bitvector
  • msammler/bool_decide_simpl_never
  • ralf/hint-mode-check
  • ralf/hint-mode-plus
  • ralf/list
  • ralf/listZ
  • ralf/map
  • ralf/union_with
  • robbert/cbn
  • robbert/f_equiv_pointwise
  • robbert/from_option
  • robbert/map_filter_True_False
  • robbert/multiset_singleton
  • robbert/naive_solver_evars
  • coq-stdpp-1.8.0
  • coq-stdpp-1.7.0
  • 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
30 results
Created with Raphaël 2.2.016Nov1530Oct27141312117653229Sep282726211915141165130Aug283229Jul2725212Jun131May30111095432130Apr2825241918141124Mar2120191817817Feb13764111Jan109216Dec151312530Nov2925242318171615227Oct24208629Sep28272524232120725Aug24231716121110983131Jul272618728Jun2726830May25231613119864312Apr118730Mar18161524Feb2022Jan1917141312Merge branch 'rm_NPeano' into 'master'mastermasterRemove reference to NPeanoMerge branch 'ralf/inv-num' into 'master'changelogReplace all uses of `inversion` by `inv`.Fix uses of legacy `inversion` in `list.factor out helper tactic for 'run on n-th hypothesis in the goal'make 'oinv 1' workmake 'inv 1' workBreak long line.Style tweak.Merge branch 'robbert/prod_swap' into 'master'Merge branch 'robbert/params_prod_map_zip' into 'master'CHANGELOG.Add `prod_swap` and some basic results for it.Missing `Params` instances for `prod_map` and `prod_zip`.Merge branch 'ralf/inv' into 'master'changeloguse the new tactics in a few spotsadd inv and oinv tactics that are basically a smarter and fixed inversion_clearMerge branch 'robbert/lt_wf_projected' into 'master'Add test case.CHANGELOG.Add `lt_wf_projected` lemmas for `nat`, `N`, `Z`.Merge branch 'ralf/wf' into 'master'Tweak line breaks.remove 'wf' alias for the standard 'well_founded'Merge branch 'ralf/solve-proper-subrelation' into 'master'style tweakswe do need mode ! and eassumption after allchangelogtry fast_reflexivity first, not lastfactor flip cleaning into a tacticmove some tactic tests so they can be run with fewer things compilingmove flip handling to inside f_equiv and solve_proper_finishsolve_proper: add support for subrelationMerge branch 'mthrow' into 'master'Add elem_of_mfail and set_unfold_elem_of_mfailUpdate changelog for MThrowUpdate comment