- Jan 17, 2017
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
-
- Jan 13, 2017
- Jan 12, 2017
-
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Jan 11, 2017
-
-
Robbert Krebbers authored
-
-
Ralf Jung authored
-
Jacques-Henri Jourdan authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Jacques-Henri Jourdan authored
-
Jacques-Henri Jourdan authored
-
Jacques-Henri Jourdan authored
-
Ralf Jung authored
Coq 8.6 Once we make Coq 8.6 mandatory, we should merge this. @robbertkrebbers I removed your `v8.6` branch (last commit: <https://gitlab.mpi-sws.org/FP/iris-coq/commit/b144f52f94c14ee5da1412b73a2d49981f9850b8>). For once, it had the wrong name (you're not talking about Iris 8.6, are you? ;-); also, all it was doing was working around a bug in Coq that has since been fixed there. See merge request !30
-
Ralf Jung authored
Unfortunately, we currently have to keep the unicode-space hack in some places because Coq still complains about the notation otherwise
-
Ralf Jung authored
This approach is originally by Robbert
-
Ralf Jung authored
There are certainly more places this is useful, but let's start with this simple test
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Jacques-Henri Jourdan authored
-
- Jan 10, 2017
- Jan 09, 2017
- Jan 08, 2017
-
-
Ralf Jung authored
-
- Jan 07, 2017
-
-
Robbert Krebbers authored
Fix fixes issue #63.
-
- Jan 06, 2017