- Apr 18, 2018
-
-
Ralf Jung authored
-
- Apr 09, 2018
-
-
Robbert Krebbers authored
Weaken axioms for BI embeddings See merge request FP/iris-coq!137
-
Ralf Jung authored
-
Jacques-Henri Jourdan authored
rename : affinely_persistently -> intuitionistically. Add lemma about monpred_at and intuitionistically.
-
Jacques-Henri Jourdan authored
-
- Apr 06, 2018
- Apr 05, 2018
-
-
Ralf Jung authored
add notation to define the PROP we use for a particular turnstile See merge request FP/iris-coq!134
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
Fixes #156
-
Robbert Krebbers authored
Extend ElimModal with Boolean flags to specify whether it operates on the… See merge request FP/iris-coq!129
-
- Apr 04, 2018
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Extend ElimModal with Boolean flags to specify whether it operates on the persistent/spatial context.
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
-
Robbert Krebbers authored
-
- Apr 03, 2018
-
-
Robbert Krebbers authored
The closing view shift's LHS mask is now universally quantified, which makes it easier to execute the closing view shift.
-
Robbert Krebbers authored
-
Ralf Jung authored
-
Ralf Jung authored
more consistent lemma naming See merge request FP/iris-coq!135
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
- Mar 31, 2018
-
-
Ralf Jung authored
-
- Mar 28, 2018
-
-
Robbert Krebbers authored
-
- Mar 27, 2018
-
-
Robbert Krebbers authored
This is a substitute for !136.
-
- Mar 24, 2018
