Merge branch 'clarify-require' into 'master'

Clarify use of Require

See merge request iris/iris!345

theories/proofmode/tactics.v

 From iris.proofmode Require Export ltac_tactics.
+(* This [Require Import] is not a no-op: it exports typeclass instances from
+these files. *)
 From iris.proofmode Require Import class_instances_bi class_instances_sbi frame_instances modality_instances.