Report an error when iIntro fails to find a forall

See merge request iris/iris!510

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.

use sep. conjunction instead of conjunction for allocation lemmas

See merge request iris/iris!508

Fix compilation with Coq 8.10

See merge request iris/iris!507

Fixes a bug from iris/iris!488

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