diff --git a/released/packages/coq-hol-light-real-with-N/coq-hol-light-real-with-N.1.0.0/opam b/released/packages/coq-hol-light-real-with-N/coq-hol-light-real-with-N.1.0.0/opam
new file mode 100644
index 000000000..ad6c4c404
--- /dev/null
+++ b/released/packages/coq-hol-light-real-with-N/coq-hol-light-real-with-N.1.0.0/opam
@@ -0,0 +1,30 @@
+opam-version: "2.0"
+synopsis: "Definition of HOL-Light real numbers in Coq using N"
+description: """
+This library provides a representation in Coq of the definition of real numbers
+in HOL-Light, using the Coq type N for natural numbers, automatically generated
+from HOL-Light using hol2dk and lambdapi.
+"""
+homepage: "https://github.com/Deducteam/coq-hol-light-real-with-N"
+dev-repo: "git+https://github.com/Deducteam/coq-hol-light-real-with-N.git"
+bug-reports: "https://github.com/Deducteam/coq-hol-light-real-with-N/issues"
+doc: "https://github.com/Deducteam/coq-hol-light-real-with-N"
+maintainer: "frederic.blanqui@inria.fr"
+authors: ["Frédéric Blanqui"]
+license: "CeCILL-2.1"
+depends: [
+  "coq" {>= "8.19"}
+]
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+tags: [
+  "keyword:HOL-Light"
+  "category:Math/Arith/Misc"
+  "category:Math/Arith/Real numbers"
+  "date:2025-01-20"
+  "logpath:HOLLight_Real"
+]
+url {
+  src: "https://github.com/Deducteam/coq-hol-light-real-with-N/archive/refs/tags/1.0.0.tar.gz"
+  checksum: "sha256=97895ee619541adf57617f23ea975489f5ceac7be718b03e7f45ac7d878cb479"
+}
diff --git a/released/packages/coq-hol-light-real-with-nat/coq-hol-light-real-with-nat.1.0.0/opam b/released/packages/coq-hol-light-real-with-nat/coq-hol-light-real-with-nat.1.0.0/opam
index 59571f472..074ef0eff 100644
--- a/released/packages/coq-hol-light-real-with-nat/coq-hol-light-real-with-nat.1.0.0/opam
+++ b/released/packages/coq-hol-light-real-with-nat/coq-hol-light-real-with-nat.1.0.0/opam
@@ -1,5 +1,5 @@
 opam-version: "2.0"
-synopsis: "Definition of HOL-Light real numbers in Coq"
+synopsis: "Definition of HOL-Light real numbers in Coq using nat"
 description: """
 This library provides a representation in Coq of the definition of real numbers
 in HOL-Light using the Coq type nat for natural numbers, automatically generated