- Jan 24, 2019
- Jan 23, 2019
-
-
Ralf Jung authoredAdded note about unicode asterisk to docs See merge request FP/iris-coq!203
-
Mackie Loeffel authored
-
Ralf Jung authored
A Coq bug printing spurious parentheses has been fixed. See merge request FP/iris-coq!197
-
Ralf Jung authored
-
- Jan 22, 2019
-
-
Hugo Herbelin authored
See Coq PR#9214.
-
Ralf Jung authored
Coq-version-specific ref files See merge request FP/iris-coq!202
-
- Jan 19, 2019
- Jan 18, 2019
-
-
Robbert Krebbers authored
-
- Jan 17, 2019
-
-
Robbert Krebbers authored
Copyedit the proof mode documentation See merge request FP/iris-coq!200
-
- Jan 15, 2019
-
-
Robbert Krebbers authored
This became broken after the nested iSpecialize MR.
-
- Jan 14, 2019
-
-
Tej Chajed authored
-
- Jan 13, 2019
-
-
Robbert Krebbers authored
Fix issue #206 Closes #206 See merge request FP/iris-coq!199
-
Robbert Krebbers authored
-
- Jan 11, 2019
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Allow `iSpecialize` to be nested. See merge request FP/iris-coq!198
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
It now supports the specialization pattern `(H spat1 .. spatn)`, which first recursively specializes the hypothesis `H` using the specialization patterns `spat1 .. spatn`.
-
Robbert Krebbers authored
This commit closes issue #192.
-
- Jan 10, 2019
-
-
Robbert Krebbers authored
-
- Jan 02, 2019
-
-
Ralf Jung authored
-
- Dec 25, 2018
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
The continuation is called with a Boolean indicating whether the hypothesis was in the intuitionistic context or not.
-
Robbert Krebbers authored
Split it up into more logical parts.
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Dec 22, 2018
-
-
Robbert Krebbers authored
-
- Dec 21, 2018
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
The unbounded fractional camera See merge request FP/iris-coq!195
-
Robbert Krebbers authored
-
