- Nov 28, 2017
-
-
Ralf Jung authored -
Ralf Jung authored
-
-
Ralf Jung authored
-
Robbert Krebbers authored
Get rid of `ofe_fun`, it was just a non-dependently typed version of `iprod` See merge request FP/iris-coq!88
-
Robbert Krebbers authored
-
- Nov 27, 2017
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
In same spirit as the other 'primitive' types like `option`, `prod`, ...
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Nov 24, 2017
-
-
Ralf Jung authored
-
Ralf Jung authored
do not make use of wp_bind_inv unnecessarily See merge request FP/iris-coq!87
-
Ralf Jung authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
-
Ralf Jung authored
-
Robbert Krebbers authored
Use solely canonical structures for language hierarchy. See merge request FP/iris-coq!90
-
- Nov 23, 2017
-
-
Ralf Jung authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
Fix some typos in Section 9.2 (Boxes) in the docs. See merge request FP/iris-coq!89
-
Robbert Krebbers authored
It can be infered now.
-
Robbert Krebbers authored
-
Dan Frumin authored
-
- Nov 22, 2017
-
-
Robbert Krebbers authored
It used to be an inline pattern match. This also restores compatibility with Coq 8.6.1.
-
Robbert Krebbers authored
-
Ralf Jung authored
saved predicates: use ofe_fun, not ofe_mor See merge request FP/iris-coq!86
-
- Nov 21, 2017
-
-
Robbert Krebbers authored
-
Ralf Jung authored
-
Robbert Krebbers authored
-
