Merge branch 'patch-1' into 'master'

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

See merge request !3

README.md

@@ -16,11 +16,12 @@ Then install with `opam install coq-iris-string-ident`.
 
 ## Usage
 
-Simply require this file before using the feature in the proof mode:
+Before using the feature in the proof mode, simply import this file _after_
+the proof mode:
 
 ```coq
-From iris_string_ident Require ltac2_string_ident.
-From iris.proofmode Require Import tactics intro_patterns.
+From iris.proofmode Require Import tactics.
+From iris_string_ident Require Import ltac2_string_ident.
 
 Lemma sep_demo {PROP: sbi} (P1: PROP)  (P2 P3: Prop) (Himpl: P2 -> P3) :
   P1 ∗ ⌜P2⌝ -∗ P1 ∗ ⌜P3⌝.