From dbe9e6ea8183e303d5a3b38cc226054741a2b484 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sat, 1 Feb 2020 14:10:29 +0100
Subject: [PATCH] Clarify use of Require

---
 theories/proofmode/tactics.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index dad2afd87..22ece1b62 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1,2 +1,4 @@
 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.
-- 
GitLab