Re-implement passing identifier back to Ltac1

See merge request !5

Add tests and test infrastructure

See merge request !4

This implementation avoids use of Unsafe, so it is compatible with v8.11
and forward, and also has the benefit of being simpler.

Correct usage instructions: replace `Require` with `Require Import`

See merge request !3

The fact that `Require` seems to work is a misfeature
(https://github.com/coq/coq/issues/12206). Worse, unlike you'd expect from
`Require`, indirect `Require` doesn't work.

opam: require minimum Iris version (fix #2)

Closes #2

See merge request !2

make LICENSE consistent with Iris

See merge request !1