- Oct 18, 2017
-
-
Ralf Jung authored -
Ralf Jung authored
-
Ralf Jung authored
-
Jacques-Henri Jourdan authored
-
- Oct 12, 2017
-
-
Ralf Jung authored
-
- Oct 10, 2017
-
-
Robbert Krebbers authored
Introduce a connective `ilocked` to stop `iNext` and `iFrame`. See merge request FP/iris-coq!67
-
Robbert Krebbers authored
-
Ralf Jung authored
use primitive projections for our mixins See merge request FP/iris-coq!69
-
Ralf Jung authored
-
Ralf Jung authored
Remove an unused argument for `newcounter_mono_spec`. See merge request FP/iris-coq!70
-
Dan Frumin authored -
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
- Oct 09, 2017
- Oct 07, 2017
-
-
Ralf Jung authored
-
- Oct 05, 2017
-
-
Robbert Krebbers authored
update stdpp See merge request FP/iris-coq!68
-
Hai Dang authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
-
- Oct 04, 2017
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
-
- Sep 28, 2017
-
-
Robbert Krebbers authored
-
Ralf Jung authored
-
- Sep 27, 2017
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
This causes a bit of backwards incompatibility: it may now succeed with later stripping below unlocked/TC transparent definitions. This problem actually occured for `wsat`.
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
Common tactic machinery for symbolic execution of pure reductions See merge request FP/iris-coq!64
-
Ralf Jung authored
-
- Sep 26, 2017
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
