Add twp_ lemmas for the arrays.

See merge request iris/iris!374

Fix issue #288: iExists fails if goal after the existential quantifier is an evar

Closes #288

See merge request iris/iris!372

Linear invariant counterexample, and more cinv rules

Closes #132

See merge request iris/iris!368

Document CoqIDE Unicode binding configuration

Closes #269

See merge request iris/iris!347

Tej Chajed authored Feb 06, 2020 and Robbert Krebbers committed Feb 06, 2020

Fixes #269.

Make `big_op{L,M}_gen_proper_2` stronger

See merge request iris/iris!363

another variant of the linear-inv counterexample, based on an accessor that gives back the token earlier

heap_lang/lifting.v: Don't run auto on hopeless goals

See merge request iris/iris!369

Paolo G. Giarrusso authored Feb 05, 2020 and Robbert Krebbers committed Feb 05, 2020

Those goals happen to be solvable by [done] as well, so use that.

I also dropped some inconsistent line breaks.

Added variant of big_sepL_lookup_acc which allows updating the value

See merge request iris/iris!365

Fix unexpected implicit binder warning

See merge request iris/iris!367

Tej Chajed authored Feb 02, 2020 and Ralf Jung committed Feb 02, 2020

Coq master is stricter about checking for meaningless implicit binders;
see https://github.com/coq/coq/pull/10202.

Better handling of persistent results in `iDestruct`, `iPoseProof`, `iAssert` and friends

See merge request iris/iris!341

Make handling of `AddModal` in `tac_specialize_frame` consistent with that in `tac_specialize_assert`.