This reverts commit bc8e2d15.
We already ignore those in the tex folders. We don't want global ignores for them.
Set `Hint Mode` for `inG`.
See merge request !330
See merge request !324
There is no need to include the `(∃ P', □ ▷ (P ↔ P') ...` since we
get closure under `▷ □ ↔` from regular invariants.
Added a stronger version of cinv_open_strong
See merge request !326
Simplify definition of invariant model.
See merge request !327
Due to the new semantic invariants (!319) we no longer need to
close the model (i.e. `inv_def`) to be contractive, the semantic
invariant definition (i.e. `inv`) is already contractive.
Update gitignore for compatibility with Coq master
See merge request !325
See https://github.com/coq/coq/pull/10947 (.coqdeps.d now uses the name
of the Coq Makefile) and https://github.com/coq/coq/pull/8642 (Coq now
generates empty interface files *.vos when compiling).
move docs around
See merge request !323
make gFunctors_lookup a local coercion to avoid ambiguous paths
See merge request !322
Update version in URL for Iris appendix
See merge request !321
I'd consider (in addition or alternative) to link to a new
http://plv.mpi-sws.org/iris/appendix-master.pdf, always matching the latest
Soundness lemma for internal equality of `uPred`.
See merge request !315