Merge Requests · Iris / stdpp

Remove dead type classes and notations.

!197 · opened Oct 28, 2020 by Robbert
- MERGED
- 1
- 5
updated Oct 28, 2020
Added sig_finite (and elem_of_list_fmap_inj, proj1_inj_pi)

!164 · opened Jun 12, 2020 by sarahzrf
- MERGED
- 1
- 10
updated Jun 18, 2020
Fix `Export` order for `length`. Remove `length` hack in strings.

!129 · opened Mar 24, 2020 by Robbert
- MERGED
- 1
- 28
updated Apr 11, 2020
More lemmas for `filter` w.r.t. maps

!96 · opened Sep 11, 2019 by Robbert
- MERGED
- 1
- 2
updated Sep 12, 2019
Additionally lemmas for insert, nth, take, and list_find

!55 · opened Feb 08, 2019 by Hai Dang
- MERGED
- 1
- 15
updated Feb 21, 2019
Add explicit Global to hints at top level

!202 · opened Nov 20, 2020 by Tej Chajed
- MERGED
- 5
updated Nov 23, 2020
Set `Hint Mode` for `pretty`.

!201 · opened Nov 12, 2020 by Robbert
- MERGED
- 2
updated Nov 12, 2020
Pretty-print 0 as "0" for N, Z, and nat

!200 · opened Nov 09, 2020 by Robbert
- MERGED
- 3
updated Nov 11, 2020
Add lemmas about `list_to_map`

!199 · opened Nov 09, 2020 by Simon Friis Vindum
- MERGED
- 6
updated Nov 10, 2020
add a function to obtain a set with all elements of a finite type

!196 · opened Oct 28, 2020 by Ralf Jung
- MERGED
- 5
updated Oct 29, 2020
add dom_insert_lookup

!195 · opened Oct 28, 2020 by Ralf Jung
- MERGED
- 4
updated Oct 28, 2020
Add map_fmap_union for FinMap

!194 · opened Oct 20, 2020 by Tej Chajed
- MERGED
- 2
updated Oct 21, 2020
Avoid relying on implicit instance generalization, and name some instances.

!193 · opened Oct 15, 2020 by Robbert
- MERGED
- 0
updated Oct 15, 2020
update Makefile

!191 · opened Oct 06, 2020 by Ralf Jung
- MERGED
- 1
updated Oct 06, 2020
Drop support for Coq 8.8 and 8.9

!190 · opened Oct 06, 2020 by Ralf Jung
- MERGED
- 3
updated Oct 13, 2020
Extend the theory of positive rationals `Qp` 1 of 1 task completed

!188 · opened Oct 03, 2020 by Robbert
- MERGED
- 106
updated Oct 31, 2020
Add Qp lemmas

!187 · opened Oct 02, 2020 by Simon Friis Vindum
- MERGED
- 14
updated Oct 02, 2020
add version of Qp_lower_bound that returns less-than facts

!186 · opened Oct 01, 2020 by Ralf Jung
- MERGED
- 1
updated Oct 01, 2020
Add "options" file

!185 · opened Sep 16, 2020 by Ralf Jung
- MERGED
- 13
updated Sep 29, 2020
Switch to strict bulleting everywhere

!184 · opened Sep 14, 2020 by Tej Chajed
- MERGED
- 21
updated Sep 15, 2020