Merge requests · Iris / stdpp

lookup_gset_to_gmap: use decide rather than guard

!436 · created Dec 15, 2022 by Ralf Jung
- CLOSED
- 8
updated Dec 22, 2022
Introduce `set_bind` and associated lemmas.

!383 · created May 30, 2022 by Dan Frumin
- CLOSED
- 1
- 24
updated Aug 09, 2022
Add the feed revert, efeed revert, efeed inversion, and efeed destruct tactics

!389 · created Jul 26, 2022 by Michael Sammler
- CLOSED
- 20
updated Aug 09, 2022
Add `set_map_2` and associated lemmas.

!381 · created May 23, 2022 by Dan Frumin
- CLOSED
- 13
updated May 30, 2022
Draft: Overlay for PR#15518

!365 · created Jan 20, 2022 by Matthieu Sozeau
- CLOSED
- 14
updated May 06, 2022
WIP: bitvector library

!250 · created Apr 15, 2021 by Michael Sammler S-draft
- CLOSED
- 40
updated Dec 08, 2021
Add Arguments bool_decide : simpl never

!331 · created Oct 15, 2021 by Michael Sammler
- CLOSED
- 10
updated Oct 25, 2021
Draft: use SProp for well-formedness condition in Pmap and gmap

!189 · created Oct 05, 2020 by Tej Chajed S-waiting-for-review
- CLOSED
- 40
updated Jul 27, 2021
strengthened solve_decision ltac

!295 · created Jul 14, 2021 by Abhishek Anand
- CLOSED
- 4
updated Jul 14, 2021
check for missing 'Hint Mode'

!272 · created Jun 03, 2021 by Ralf Jung S-blocked
- CLOSED
- 2
updated Jun 17, 2021
Multiset set notation 2 of 2 checklist items completed

!232 · created Mar 11, 2021 by Robbert Krebbers
- CLOSED
- 18
updated Apr 20, 2021
Random collection of lemmas from RefinedC

!244 · created Apr 14, 2021 by Michael Sammler
- CLOSED
- 9
updated Apr 15, 2021
WIP: Pretty-print 0 as "0" for N, Z, and nat

!198 · created Nov 06, 2020 by Tej Chajed
- CLOSED
- 6
updated Nov 10, 2020
Add a way to disable typeclass search in `Program` obligations

!149 · created Apr 21, 2020 by Paolo G. Giarrusso
- CLOSED
- 11
updated Nov 03, 2020
Draft: Drop misleading gmultiset_simple_set instance

!192 · created Oct 10, 2020 by Paolo G. Giarrusso
- CLOSED
- 9
updated Oct 12, 2020
[simpl_map]: avoid using [rewrite .. by ..]

!177 · created Jul 20, 2020 by Armaël Guéneau
- CLOSED
- 4
updated Sep 29, 2020
fix various uses of generated names

!181 · created Aug 29, 2020 by Ralf Jung
- CLOSED
- 3
updated Aug 30, 2020
add singleton_insert_empty

!168 · created Jun 29, 2020 by Ralf Jung
- CLOSED
- 9
updated Jun 29, 2020
Adapt w.r.t. coq/coq#12512.

!165 · created Jun 15, 2020 by Ghost User
- CLOSED
- 24
updated Jun 17, 2020
overlay for coq/coq#12162

!153 · created Apr 29, 2020 by Olivier Laurent
- CLOSED
- 25
updated May 07, 2020