diff --git a/coq-iris-heap-lang.opam b/coq-iris-heap-lang.opam
index 7a6809ef36b01a7731b1af9b8b614442c5d7a372..7d671368c264d9b13d64c68e08343f4b39de1da5 100644
--- a/coq-iris-heap-lang.opam
+++ b/coq-iris-heap-lang.opam
@@ -9,8 +9,12 @@ version: "dev"
 
 synopsis: "The canonical example language for Iris"
 description: """
-This package provides the iris.heap_lang Coq module.
+This package defines HeapLang, a concurrent lambda calculus with references, and
+uses Iris to build a program logic for HeapLang programs.
 """
+tags: [
+  "logpath:iris.heap_lang"
+]
 
 depends: [
   "coq-iris" {= version}
diff --git a/coq-iris.opam b/coq-iris.opam
index f098ca7f42aaa17e955272c25dcf9ef5f1af5f1a..125b0e84498c5e2651f052b56ff7133cba8ec6fd 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -9,9 +9,22 @@ version: "dev"
 
 synopsis: "A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs"
 description: """
-This package provides the following Coq modules:
-iris.prelude, iris.algebra, iris.si_logic, iris.bi, iris.proofmode, iris.base_logic, iris.program_logic.
+Iris is a framework for reasoning about the safety of concurrent programs using
+concurrent separation logic. It can be used to develop a program logic, for
+defining logical relations, and for reasoning about type systems, among other
+applications. This package includes the base logic, Iris Proof Mode (IPM) /
+MoSeL, and a general language-independent program logic; see coq-iris-heap-lang
+for an instantiation of the program logic to a particular programming language.
 """
+tags: [
+  "logpath:iris.prelude"
+  "logpath:iris.algebra"
+  "logpath:iris.si_logic"
+  "logpath:iris.bi"
+  "logpath:iris.proofmode"
+  "logpath:iris.base_logic"
+  "logpath:iris.program_logic"
+]
 
 depends: [
   "coq" { (>= "8.12" & < "8.15~") | (= "dev") }