- Dec 13, 2022
-
-
Paolo G. Giarrusso authored
Motivated by https://mattermost.mpi-sws.org/iris/pl/cz6f4bxwsir78jkunk7nt3bawo.
-
- Dec 12, 2022
-
-
Robbert Krebbers authored
add map_zip_with_empty lemmas See merge request iris/stdpp!430
-
Ralf Jung authored
-
- Dec 05, 2022
- Nov 30, 2022
-
-
Ralf Jung authored
-
Ralf Jung authored
Tweak `f_equiv` to use `reflexivity` in a way similar to `f_equal`. See merge request iris/stdpp!428
-
- Nov 29, 2022
-
-
Ralf Jung authored
make solve_ndisj work on goals of the form 'X1 ∪ X2 ## Y' See merge request iris/stdpp!427
-
Robbert Krebbers authored
-
Ralf Jung authored
-
-
Ralf Jung authored
Use `notypeclasses refine` for `TCIf` and `TCNoBackTrack`. See merge request iris/stdpp!426
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Nov 25, 2022
- Nov 24, 2022
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Add tactic `tc_solve`. See merge request iris/stdpp!425
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Nov 23, 2022
-
-
Michael Sammler authored
Fix unfolding logic of bv_simplify See merge request iris/stdpp!411
-
- Nov 18, 2022
-
-
Robbert Krebbers authored
Use `eauto` as default for `set_solver`. See merge request iris/stdpp!420
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
add gset_to_gmap_to_list See merge request iris/stdpp!422
-
- Nov 17, 2022
- Nov 16, 2022
-
-
Ralf Jung authored
-
-
Robbert Krebbers authored
Use `-native-compiler no` to make sure we do not rely on (bugs) in `native_compute`. See merge request iris/stdpp!419
-
Robbert Krebbers authored
-
Ralf Jung authored
-
- Nov 15, 2022
-
-
Ralf Jung authored
-
- Nov 02, 2022
-
-
Ralf Jung authored
Fix bitvector tests for coq#16748 See merge request iris/stdpp!421
-
Michael Sammler authored
-
- Oct 20, 2022
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Oct 08, 2022
-
-
Ralf Jung authored
Add some type annotations for prepare for `Hint Mode` for `Equiv`. See merge request iris/stdpp!418
-
