Issues · Iris / stdpp · GitLab

Associativity of insert notation is awkard: `<[ k := v ]> m`

#59 · opened Apr 01, 2020 by Gregory Malecha
- 9
updated Apr 03, 2020
stdpp breaks setoid rewriting

#58 · opened Mar 30, 2020 by sarahzrf
- 7
updated Apr 01, 2020
stdpp.base.decide := Coq.Classes.DecidableClass.decide?

#51 · opened Feb 11, 2020 by Abhishek Anand
- 5
updated Feb 17, 2020
Make coPset operations TC opaque

#48 · opened Feb 10, 2020 by Robbert
- 3
updated Feb 18, 2020
solve_ndisj taking a long time

#47 · opened Dec 03, 2019 by Jonas Kastberg
- 1
updated Dec 04, 2019
`Hint Mode` for `QuoteLookup` and `Quote`

#44 · opened Sep 16, 2019 by Dan Frumin
- 4
updated Sep 19, 2019
Provide a better `inversion` tactic

#40 · opened Aug 23, 2019 by Robbert
- 3
updated Aug 24, 2019
Create list of tactics provided by std++

#39 · opened Jul 04, 2019 by Robbert
- 1
updated Jul 04, 2019
Add a test for solve_proper on a unary function

#38 · opened Jul 02, 2019 by Ralf Jung
- 0
updated Jul 02, 2019
Extend `solve_proper` to better handle HO functions

#37 · opened Jul 02, 2019 by Robbert
- 2
updated Feb 13, 2020
Unify case_bool_decide / case_decide

#35 · opened Jun 22, 2019 by Ralf Jung
- 0
updated Jun 22, 2019
Map singleton notation overlaps with Coq record syntax

#32 · opened Jun 10, 2019 by Ralf Jung
- 0
updated Jun 10, 2019
Addition is only declared as `Commutative` in iris

#31 · opened Jun 04, 2019 by Paolo G. Giarrusso
- 1
updated Jun 14, 2019
More generic `FMap` type class that also supports collections

#21 · opened Oct 04, 2018 by Robbert wishlist
- 5
updated Nov 07, 2019
What about `Universe Minimization ToSet`?

#19 · opened Jun 09, 2018 by Ralf Jung
- 1
updated Jun 09, 2018
Notation for type class logic connectives as `TCAnd`, `TCOr`, ...

#11 · opened Feb 08, 2018 by Robbert
- 22
updated Feb 20, 2018
Inconsistent `RewriteRelation` instances

#10 · opened Jan 10, 2018 by Robbert
- 2
updated Jul 03, 2019
Make more consistent use of coqdoc for web doc

#9 · opened Dec 07, 2017 by Ralf Jung
- 14
updated Jun 17, 2019
`f_equiv` with different functions in head position produces a Leibniz equality

#8 · opened Dec 01, 2017 by Robbert
- 1
updated Aug 22, 2019
Improve support of simplify_option_eq (and simplify_map_eq?) for setoids

#7 · opened Nov 13, 2017 by Robbert wishlist
- 0
updated Feb 20, 2019