diff --git a/coq-iris-heap-lang.opam b/coq-iris-heap-lang.opam
index 42bd1d233fbcf786a7337594d837d852b159c0a7..7a6809ef36b01a7731b1af9b8b614442c5d7a372 100644
--- a/coq-iris-heap-lang.opam
+++ b/coq-iris-heap-lang.opam
@@ -7,7 +7,7 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
 version: "dev"
 
-synopsis: "HeapLang is the canonical example language for Iris"
+synopsis: "The canonical example language for Iris"
 description: """
 This package provides the iris.heap_lang Coq module.
 """
diff --git a/coq-iris.opam b/coq-iris.opam
index dbf8491f0e232af2602ba83e14cd35965a38535d..c375c3359bc778a8fc7bd9edb749e83cf14d1e03 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -7,7 +7,7 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
 version: "dev"
 
-synopsis: "Iris is a Higher-Order Concurrent Separation Logic Framework with support for interactive proofs"
+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.