- 06 Sep, 2021 7 commits
-
-
Ralf Jung authored
-
Ralf Jung authored
Optimize iIntoEmpValid See merge request iris/iris!729
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Armaël Guéneau authored
With large proof contexts and lemmas with many forall quantifiers, iIntoEmpValid can become quite slow. This makes it go faster by adding "fast paths" for the -> and forall cases, gated by Ltac pattern matching (which is faster than trying to unify with refine and fail).
-
Robbert Krebbers authored
Fix and improve `iSpecialize` auto framing error message. Closes #432 See merge request iris/iris!730
-
- 05 Sep, 2021 3 commits
-
-
Ralf Jung authored
make binary wand/view shift connectives 'block' formated See merge request iris/iris!727
-
Ralf Jung authored
-
Ralf Jung authored
-
- 03 Sep, 2021 3 commits
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
This closes issue #432.
-
- 01 Sep, 2021 2 commits
- 10 Aug, 2021 3 commits
-
-
Ralf Jung authored
na_invariants: deduplicate proof of fresh_inv_name See merge request iris/iris!728
-
Paolo G. Giarrusso authored
Debatable, but the proof context of `na_inv_alloc` writes `ε` instead of `CoPSet ∅`.
-
Paolo G. Giarrusso authored
-
- 31 Jul, 2021 1 commit
-
-
Ralf Jung authored
Add generalized implication lemma for big_sepM See merge request iris/iris!697
-
- 30 Jul, 2021 3 commits
-
-
Simon Friis Vindum authored
-
-
Simon Friis Vindum authored
-
- 29 Jul, 2021 3 commits
- 28 Jul, 2021 9 commits
-
-
Ralf Jung authored
-
Robbert Krebbers authored
-
Ralf Jung authored
Printing improvements See merge request iris/iris!726
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
use iris.proofmode.proofmode as the new root module for the proofmode See merge request iris/iris!724
-
Ralf Jung authored
-
Ralf Jung authored
to avoid bad regressions, some other notations also ha to be tweaked
-
Ralf Jung authored
-
- 27 Jul, 2021 4 commits
-
-
Ralf Jung authored
-
Robbert Krebbers authored
-
Jacques-Henri Jourdan authored
-
Jacques-Henri Jourdan authored
-
- 26 Jul, 2021 2 commits
-
-
Robbert Krebbers authored
-
Ralf Jung authored
-