Commits · e3a6f3ef0fe43ac888b83fecb5a895ddb1b364a1 · Iris / stdpp

Jan 27, 2025
- Merge branch 'marijnvanwezel/properties_of_head' into 'master' · e3a6f3ef
  Robbert Krebbers authored 2 months ago
  
  Add lemmas about `last` and `head`: `last_app_or`, `head_app_or`, and `head_app`. See merge request !583
  e3a6f3ef
- Add lemmas about `last` and `head`: `last_app_or`, `head_app_or`, and `head_app`. · bb309359
  Marijn van Wezel authored 2 months ago and Robbert Krebbers committed 2 months ago
  
  bb309359
Jan 25, 2025
- bump to Coq 8.20.1 · db6bf153
  Ralf Jung authored 2 months ago
  
  db6bf153
- declare compatibility with Rocq 9.0 · 9b19c60c
  Ralf Jung authored 2 months ago
  
  9b19c60c
Jan 23, 2025
- fix changelog position for lookup_total_fmap · 9c125edf
  Ralf Jung authored 2 months ago
  
  9c125edf
Jan 17, 2025
- Merge branch 'robbert/lookup_total_fmap' into 'master' · 9e1cd491
  Ralf Jung authored 2 months ago
  
  Add lemma `lookup_total_fmap`. See merge request !530
  9e1cd491
- CHANGELOG. · ea152947
  Robbert Krebbers authored 1 year ago and Ralf Jung committed 2 months ago
  
  ea152947
- Add lemma `lookup_total_fmap`. · f46380bd
  Robbert Krebbers authored 1 year ago and Ralf Jung committed 2 months ago
  
  f46380bd
Dec 05, 2024
- Merge branch 'marijnvanwezel/gmultiset_bind' into 'master' · df46059d
  Ralf Jung authored 4 months ago
  
  Add `gmultiset_disj_union_list` See merge request !580
  df46059d
- Add `gmultiset_disj_union_list` · 144a07ef
  Marijn van Wezel authored 4 months ago and Ralf Jung committed 4 months ago
  
  144a07ef
Oct 30, 2024
- release version 1.11 · ecc41d2f
  Ralf Jung authored 5 months ago
  
  View commits for tag coq-stdpp-1.11.0 coq-stdpp-1.11.0
  
  ecc41d2f
- changelog spacing · 14c7a553
  Ralf Jung authored 5 months ago
  
  14c7a553
- changelog tweaks · d1862ff9
  Ralf Jung authored 5 months ago
  
  d1862ff9
- Merge branch 'master' into 'master' · e4733be5
  Ralf Jung authored 5 months ago
  
  Update to version 1.11.0 See merge request !579
  e4733be5
- Update to version 1.11.0 · 12c02964
  Jesper Bengtson authored 5 months ago and Ralf Jung committed 5 months ago
  
  12c02964
- Merge branch 'cprod' into 'master' · 5297f7c9
  Ralf Jung authored 5 months ago
  
  Add cartesian products to all concrete set types See merge request !576
  5297f7c9
- Add cartesian products to all concrete set types · 34c1e56d
  Thibaut Pérami authored 5 months ago and Ralf Jung committed 5 months ago
  
  34c1e56d
- Merge branch 'ralf/propset-notation' into 'master' · 96839810
  Ralf Jung authored 5 months ago
  
  make levels consistent between propset notation and singleton notation See merge request !578
  96839810
Oct 24, 2024
- make levels consistent between propset notation and singleton notation · d25bd6a6
  Ralf Jung authored 5 months ago
  
  d25bd6a6
- silence some warnings on coq.dev that we cannot fix yet · f3091cc3
  Ralf Jung authored 5 months ago
  
  f3091cc3
Oct 21, 2024
- Merge branch 'marijn/gmultiset_map' into 'master' · 4d307c87
  Ralf Jung authored 5 months ago
  
  Add `gmultiset_map` and associated lemmas See merge request !577
  4d307c87
Oct 18, 2024
- CHANGELOG. · 862e4bc5
  Robbert Krebbers authored 5 months ago
  
  862e4bc5
- Version of `gmultiset_map` that avoids converting to lists. · bfc40224
  Robbert Krebbers authored 5 months ago
  
  bfc40224
Oct 17, 2024
- Move definition to top · 63835cb3
  Marijn van Wezel authored 5 months ago
  
  Unverified
  
  63835cb3
- Rewrite injectivity lemma to instance of Inj · f2098383
  Marijn van Wezel authored 5 months ago
  
  Unverified
  
  f2098383
- Improve styling · e7405db5
  Marijn van Wezel authored 5 months ago
  
  Unverified
  
  e7405db5
- Slightly simplify proof · 2cbe4b4f
  Marijn van Wezel authored 5 months ago
  
  Unverified
  
  2cbe4b4f
- Use unicode arrow · 3f7421c7
  Marijn van Wezel authored 5 months ago
  
  Unverified
  
  3f7421c7
Oct 10, 2024
- Add lemma about injectivity of gmultiset_map when 'f' is injective · 65f28290
  Marijn van Wezel authored 5 months ago
  
  65f28290
- Actually give an explicit name to the IH · 88a3baa1
  Marijn van Wezel authored 5 months ago
  
  88a3baa1
- Explicitly name IH · 70772e14
  Marijn van Wezel authored 5 months ago
  
  70772e14
- Remove superfluous type hints · a1d0c311
  Marijn van Wezel authored 5 months ago
  
  a1d0c311
- Move to section and add lemmas · bb981de3
  Marijn van Wezel authored 5 months ago
  
  bb981de3
Oct 09, 2024
- Add definition for `gmultiset_map` · 65cf7d06
  Marijn van Wezel authored 6 months ago
  
  65cf7d06
Oct 02, 2024
- add comment in _CoqProject · 1fa37d0a
  Ralf Jung authored 6 months ago
  
  1fa37d0a
- Merge branch 'robbert/map_Forall2_nested' into 'master' · 2dd41ab5
  Robbert Krebbers authored 6 months ago
  
  Enable `map_Forall2` to be used in nested inductive relations See merge request !575
  2dd41ab5
Sep 29, 2024
- Also add a test for `map_Forall`. · 5e36b905
  Robbert Krebbers authored 6 months ago
  
  5e36b905
Sep 28, 2024
- Enable `map_Forall2` to be used in nested inductive relations. · 6bb1fc01
  Robbert Krebbers authored 6 months ago
  
  6bb1fc01
Sep 11, 2024
- sync dune flags · bc4fce09
  Ralf Jung authored 6 months ago
  
  bc4fce09
- Merge branch 'robbert/deprecate_rev_length' into 'master' · 6a0896a2
  Ralf Jung authored 6 months ago
  
  Unsilence deprecation warning regarding list lemmas. See merge request !574
  6a0896a2