The error handling for `iIntro (?)` and similar tactics didn't correctly
report failures when the goal couldn't be turned into a universal
quantifier. This is something missing from !482 due to no test
triggering the error.

add a simple logic-level ghost_var library

See merge request iris/iris!488

This reverts commit 59280f68.
It was not actually needed.

wtf, sed?!??

Fix argument order in comment.

See merge request iris/iris!506

Isomorphism and validy restriction constructions for cameras.

See merge request iris/iris!504

rename `agree_op_{inv,invL}'` to `to_agree_op_{inv,invL}`

See merge request iris/iris!505

improve [core] docs

See merge request iris/iris!503

Fixes #345

The old code contained a bunch of unused spaghetti that was not cleaned up
after a refactoring.

@jihgfee menaged to trigger a wrong code path in the old code, but I failed
to turn his test case into a self-contained one.

add conversions between functors

Closes #342

See merge request iris/iris!498

add options file for library-wide configuration

Closes #66

See merge request iris/iris!491

add internal_eq_entails uPred law

See merge request iris/iris!499

Document Makefile flags NO_TEST and MAKE_REF together

See merge request iris/iris!500

Use simple variables in Makefile

See merge request iris/iris!501