`iDestruct H as "H1 H2"` produces an error that says the pattern should
contain exactly one proper introduction pattern. When multiple patterns
are provided, due to Ltac variable shadowing iDestructHypFindPat was
instead reporting only the first pattern in the error message (and even
that was printed as the parsed AST rather than the original string).

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