- May 04, 2019
-
-
Nitpick, yes, but I've seen the complaint enough times today to bother. That complaint is only useful to maintainers, and it's even in color. ``` [WARNING] Failed checks on coq-iris-builddep package definition from source at file:///Users/pgiarrusso/git/Coq/0IRIS-SWITCH/iris/build-dep: error 57: Synopsis and description must not be both empty ```
-
Ralf Jung authored
-
- May 02, 2019
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- May 01, 2019
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Notably, `big_andL_andL` and `big_andL_and` where a ⊣⊢ and ⊢ version of the same lemma. I favored the `big_opL_op` naming scheme.
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Allow multiple arguments in `iEval .. in` and `iSimpl in`. Closes #238 See merge request iris/iris!237
-
Dan Frumin authored
-
Dan Frumin authored
-
- Apr 30, 2019
-
-
Robbert Krebbers authored
-
- Apr 29, 2019
-
-
Robbert Krebbers authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
Fix documentation for ofe_funR See merge request iris/iris!236
-
Paolo G. Giarrusso authored
This comment wasn't updated after 866cad62.
-
- Apr 27, 2019
-
-
Robbert Krebbers authored
Avoid conversion after only reducing goal. See merge request iris/iris!235
-
Robbert Krebbers authored
-
Janno authored
-
- Apr 26, 2019
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Apr 25, 2019
-
-
-
Robbert Krebbers authored
-
- Apr 24, 2019
-
-
Robbert Krebbers authored
-
Ralf Jung authored
-
- Apr 23, 2019
-
-
Robbert Krebbers authored
-
- Apr 17, 2019
-
-
Paolo G. Giarrusso authored
-
Paolo G. Giarrusso authored
If Ralf didn't know it, I guess it deserves a name. This is the first I got, feel free to improve.
-
Paolo G. Giarrusso authored
-
Paolo G. Giarrusso authored
-
Robbert Krebbers authored
-
- Apr 15, 2019
-
-
Paolo G. Giarrusso authored
That's the documentation I'd have wanted to see, and viceversa the lack of this rule implied (to me) that this wouldn't work.
-
- Apr 08, 2019
-
-
Ralf Jung authored
Nicer soundness for our update modalities See merge request iris/iris!230
-
- Apr 07, 2019
-
-
Robbert Krebbers authored
Mentioned big_sepL2/sepM2 in the changelog. See merge request iris/iris!232
-
Dan Frumin authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
The `2: { ... }` syntax is not yet supported there.
-