diff --git a/released/packages/coq-simple-io/coq-simple-io.1.10.0/opam b/released/packages/coq-simple-io/coq-simple-io.1.10.0/opam
new file mode 100644
index 000000000..a9f9f54a9
--- /dev/null
+++ b/released/packages/coq-simple-io/coq-simple-io.1.10.0/opam
@@ -0,0 +1,39 @@
+opam-version: "2.0"
+maintainer: "Li-yao Xia <lysxia@gmail.com>"
+authors: [ "Li-yao Xia" "Yishuai Li" ]
+homepage: "https://github.com/Lysxia/coq-simple-io"
+bug-reports: "https://github.com/Lysxia/coq-simple-io/issues"
+license: "MIT"
+dev-repo: "git+https://github.com/Lysxia/coq-simple-io.git"
+build: [
+  ["dune" "subst"] {dev}
+  [ "dune" "build" "-p" name "-j" jobs "@install" ]
+]
+depends: [
+  "dune" {>= "3.7"}
+  "ocaml" {>= "4.08.0"}
+  "ocamlfind"
+  "coq" {>= "8.12~" & < "8.21~"}
+  "coq-ext-lib" {>= "0.10.0"}
+  "ocamlbuild" {with-test & >= "0.9.0"}
+  "cppo" {build & >= "1.6.8"}
+]
+tags: [
+  "date:2024-09-16"
+  "logpath:SimpleIO"
+  "keyword:extraction"
+  "keyword:effects"
+]
+synopsis: "IO monad for Coq"
+description: """
+This library provides tools to implement IO programs directly in Coq, in a
+similar style to Haskell. Facilities for formal verification are not included.
+
+IO is defined as a parameter with a purely functional interface in Coq,
+to be extracted to OCaml. Some wrappers for the basic types and functions in
+the OCaml Stdlib module are provided. Users are free to define their own
+APIs on top of this IO type."""
+url {
+  src: "https://github.com/Lysxia/coq-simple-io/archive/1.10.0.tar.gz"
+  checksum: "sha512=004bc44e42d03f9d936fb512191a4e547a228a7db233b1b7aa244f4d8c2d893f2fc9f263008ad72a38b82465dd56f78d92005e0aca626a99d30ad08ec7e7afd8"
+}