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

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.

LGTM.

@Blaisorblade can you also make a PR for iris-examples to adjust our usage there?

if A performs ::=, B requires A, and C imports B, the effects of A are visible in B but not in C, despite A being Required (directly or indirectly) in both.

So I take it that if B imports A and C imports B, then the effects are visible in C as expected?

I don't think so - the intention is that ::= is an import-only effect, but there are bugs that cause it to happen on Require that make it hard to test. You can still Export ltac2_string_ident to export the effect.

Indeed, having

From iris.proofmode Require Export tactics.
From iris_string_ident Require Export ltac2_string_ident.

in a local prelude lets you worry about order only once. And thanks to the recent fix for the strings.length annoyance, that doesn't seem to break anything.

In addition to this Require Import bug, the usage in the README is wrong: if you ever re-import iris.proofmode.ltac_tactics, then string_to_ident_hook is reverted. In the example that happens due to one of the later imports.

It's still possible to use correctly, but it requires being principled about import order which is brittle.

added 1 commit

• decbb4b7 - Fix order of imports.

Compare with previous version

added 1 commit

• d88ac6aa - Drop unneeded import of intro_patterns

Compare with previous version

All done, plus a couple of nits — please take another look.

Looks good to me, thanks!

mentioned in commit 08f2cf2f

merged

mentioned in commit Blaisorblade/examples@b80f15df

mentioned in merge request examples!33 (merged)

@Blaisorblade can you also make a PR for iris-examples to adjust our usage there?

Done: examples!33 (merged).