Tej Chajed authored 5 years ago and Ralf Jung committed 5 years ago

Fixes a new warning on Coq 8.12+alpha when implicit annotations are used
in positions where they are ignored.

Adding a constructor for reflexive transitive closures into bi's

See merge request iris/iris!375

rename _open rules to _access if they are actually accessors

See merge request iris/iris!373

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 5 years ago and Robbert Krebbers committed 5 years ago

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 5 years ago and Robbert Krebbers committed 5 years ago

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