- Jul 19, 2021
-
-
Robbert Krebbers authored
Swap `curry` and `uncurry` to be consistent with Haskell and friends. Closes #76 See merge request iris/stdpp!297
-
Robbert Krebbers authored
-
Robbert Krebbers authored
This also applies to `(un)curry{3,4}`, `gmap_(un)curry`, and `h(un)curry`. This fixes issue #76. The code includes a horrible hack that should removed once support for Coq versions prior to 8.13 is dropped.
-
Ralf Jung authored
alternative implementation of mk_evar that keeps naive_solver working Closes #115 See merge request iris/stdpp!299
-
Ralf Jung authored
handle more goals in solve_ndisj See merge request iris/stdpp!294
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
- Jul 18, 2021
-
-
- Jul 17, 2021
-
-
Ralf Jung authored
-
- Jul 15, 2021
-
-
Robbert Krebbers authored
Do not call `done` recursively when solving `is_Some`. See merge request iris/stdpp!296
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
add mk_evar tactic (to replace Coq's strange evar tactic) and use it See merge request iris/stdpp!289
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
Make `done` work on `is_Some`. See merge request iris/stdpp!293
-
Robbert Krebbers authored
Fix priority of `Permutation_app'`. Closes #114 See merge request iris/stdpp!291
-
Robbert Krebbers authored
-
- Jul 03, 2021
-
-
Ralf Jung authored
add lookup_union_l See merge request iris/stdpp!292
-
Robbert Krebbers authored
-
Ralf Jung authored
-
- Jun 29, 2021
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
This is a workaround for https://github.com/coq/coq/issues/14571 This fixes #114.
-
- Jun 28, 2021
-
-
Ralf Jung authored
-
Robbert Krebbers authored
Update changelog for filter extensionality lemmas See merge request iris/stdpp!290
-
Simon Friis Vindum authored
-
- Jun 27, 2021
-
-
Ralf Jung authored
-
Robbert Krebbers authored
Make sum_inhabited_r not a copy of sum_inhabited_l See merge request iris/stdpp!288
-
Paolo G. Giarrusso authored
This existed at least as far back as iris/stdpp@361308c7, 8 years ago.
-
- Jun 26, 2021
-
-
Ralf Jung authored
rename insert_delete → insert_delete_insert; add new insert_delete matching delete_insert See merge request iris/stdpp!287
-
- Jun 25, 2021
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
Add a few set and map related lemmas See merge request iris/stdpp!284
-
Simon Friis Vindum authored
-
- Jun 24, 2021
-
-
Robbert Krebbers authored
Fix potential stack overflow related to `Pretty N`. See merge request iris/stdpp!286
-
-