- 14 Jun, 2018 6 commits
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Jacques-Henri Jourdan authored
Slightly weaker WP (i.e., easier to prove), so that we have an fupd where we did not See merge request FP/iris-coq!153
-
Jacques-Henri Jourdan authored
-
Jacques-Henri Jourdan authored
-
Jacques-Henri Jourdan authored
-
- 13 Jun, 2018 3 commits
- 12 Jun, 2018 1 commit
-
-
Ralf Jung authored
-
- 11 Jun, 2018 2 commits
- 10 Jun, 2018 12 commits
-
-
Ralf Jung authored
make the way iMod solves side-conditions consistent with iInv See merge request FP/iris-coq!155
-
Robbert Krebbers authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
-
Ralf Jung authored
-
-
Ralf Jung authored
-
Robbert Krebbers authored
-
Ralf Jung authored
-
Ralf Jung authored
-
- 09 Jun, 2018 2 commits
- 08 Jun, 2018 9 commits
-
-
Ralf Jung authored
consistently use iSolveTC to solve typeclass goals See merge request FP/iris-coq!151
-
Ralf Jung authored
also improve README
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
Added naming conventions for definitions to naming.txt See merge request FP/iris-coq!152
-
Jan authored
-
Ralf Jung authored
-
Ralf Jung authored
This avoids the proofmode to be irritated by unrelated goals with a typeclass type.
-
- 06 Jun, 2018 5 commits