Fix and test `awp_apply` error message, and also use `tactic3` everywhere

See merge request iris/iris!355

Use &&& from lazy_bool_scope instead of redefining the && notation.

See merge request iris/iris!349

fix big_sepM2_fmap and friend to work for keys other than nat

Closes #283

See merge request iris/iris!351

[doc] Fix links to doc files

Closes #281

See merge request iris/iris!350

[doc] Copy edit the heap lang documentation

See merge request !346

Fix two scripts due to bugfix in mode-checking

See merge request !344

Matthieu Sozeau authored Dec 13, 2019 and Robbert Krebbers committed Dec 13, 2019

That should not be allowed

Avoid unwanted subgoals when applying `from_assumption_exact`

See merge request !343

pointer arithmetic: properly check the operation

See merge request !340

Try getting rid of total Core typeclass

See merge request !294

Rename lemma `not_stuck_under_ectx` → `not_stuck_fill`, to be consistent with `stuck_fill`.

See merge request !339

Also refactor the proofs to make better reuse of existing lemmas.

Fix iPoseProof on recursive lemmas (fix #274)

Closes #274

See merge request !338

Paolo G. Giarrusso authored Nov 22, 2019 and Robbert Krebbers committed Nov 22, 2019

When proving `foo` through a fixpoint, Coq's guardedness checker needs to see to
which arguments `foo` is applied. Opaque lemmas applied to `foo` itself prevent
that, so make them transparent.
* Make `IntoEmpValid` lemmas transparent.
* Expose application of `IntoEmpValid` instance to its argument.
* Add comment to `tac_pose_proof`

This MR brings back the type of `tac_pose_proof` to the one it had before !329.
Hence, this seems worth a comment.