Make `iFresh` faster

See merge request iris/iris!247

Export that iPreProp is a Cofe

See merge request iris/iris!246

Generalize `iPureIntro` to support non-empty spatial contexts with just affine hypotheses.

See merge request iris/iris!241

Never used `Declare Instance`.

Add an `iSimpl in "%"` test.

See merge request iris/iris!240

Disable new warnings for Coq master

See merge request iris/iris!242

A more intuitive proof that lists from a COFE

See merge request iris/iris!239

Add synopsis so make build-dep does not complain

See merge request iris/iris!238

Paolo G. Giarrusso authored 5 years ago and Ralf Jung committed 5 years ago

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
```

This proof also more easily scales to other recursive types, like
trees etc.

Notably, `big_andL_andL` and `big_andL_and` where a ⊣⊢ and ⊢ version
of the same lemma. I favored the `big_opL_op` naming scheme.