diff --git a/packages/coq-serapi/coq-serapi.8.7.1+0.4.2/descr b/packages/coq-serapi/coq-serapi.8.7.1+0.4.2/descr
new file mode 100644
index 00000000000..c2b75a91753
--- /dev/null
+++ b/packages/coq-serapi/coq-serapi.8.7.1+0.4.2/descr
@@ -0,0 +1 @@
+Sexp Protocol for machine-based interaction with the Coq Proof Assistant.
diff --git a/packages/coq-serapi/coq-serapi.8.7.1+0.4.2/opam b/packages/coq-serapi/coq-serapi.8.7.1+0.4.2/opam
new file mode 100644
index 00000000000..158be7a7f47
--- /dev/null
+++ b/packages/coq-serapi/coq-serapi.8.7.1+0.4.2/opam
@@ -0,0 +1,29 @@
+opam-version: "1.2"
+maintainer:   "e@x80.org"
+authors:      "Emilio Jesús Gallego Arias"
+homepage:     "https://github.com/ejgallego/coq-serapi"
+bug-reports:  "https://github.com/ejgallego/coq-serapi/issues"
+dev-repo:     "git+https://github.com/ejgallego/coq-serapi.git"
+license:      "GPL 3"
+
+name: "coq-serapi"
+available: [ ocaml-version >= "4.06.0" ]
+
+# ppx depends are so strict due to the issues with ppx_import and
+# ppx_driver integration in the past.
+depends: [
+  "coq"           { >= "8.7.1+1" & < "8.8" }
+  "camlp5"
+  "cmdliner"
+  "sexplib"
+  "ocamlfind"     { build }
+  "ocamlbuild"    { build }
+  "ppx_import"    { build & >= "1.4" }
+  "ppx_deriving"  { build & >= "4.2.1" }
+  "ppx_driver"    { build & >= "v0.10.1" }
+  "ppx_sexp_conv" { build }
+]
+
+build:   [ make "-j%{jobs}%" "TARGET=native" ]
+install: [ "cp" "sertop.native" "%{bin}%/sertop" ]
+remove:  [ "rm" "-f" "%{bin}%/sertop" ]
diff --git a/packages/coq-serapi/coq-serapi.8.7.1+0.4.2/url b/packages/coq-serapi/coq-serapi.8.7.1+0.4.2/url
new file mode 100644
index 00000000000..3268d3302ac
--- /dev/null
+++ b/packages/coq-serapi/coq-serapi.8.7.1+0.4.2/url
@@ -0,0 +1,2 @@
+http: "https://github.com/ejgallego/coq-serapi/archive/8.7.1+0.4.2.tar.gz"
+checksum: "9a10e3ed7256529ed5169993c97a5a94"