diff --git a/.travis.yml b/.travis.yml
index fb67bab..ee427a6 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -7,8 +7,9 @@ services:
 
 env:
   global:
-  - OPAMJOBS="2"
+  - PACKAGE_NAME="coq-io-system"
   matrix:
+  - COQ_IMAGE="coqorg/coq:8.4"
   - COQ_IMAGE="coqorg/coq:8.5"
   - COQ_IMAGE="coqorg/coq:8.6"
   - COQ_IMAGE="coqorg/coq:8.7"
@@ -24,11 +25,8 @@ install: |
     echo \"Build triggered by ${TRAVIS_EVENT_TYPE}\"
     export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m '
     set -ex  # -e = exit on failure; -x = trace for debug
-    if [ -n \"\${COMPILER_EDGE}\" ]; then opam switch \${COMPILER_EDGE}; eval \$(opam env); fi
-    opam update -y
-    opam pin add coq-io-system.opam . --kind=path -y --no-action
-    opam pin add coq-io-system-ocaml.opam . --kind=path -y --no-action
-    opam install coq-io-system --deps-only -y --ignore-constraints-on=coq-io-system-ocaml
+    opam update
+    opam pin add ${PACKAGE_NAME}.opam . --kind=path --no-action
     opam config list
     opam repo list
     opam pin list
@@ -42,7 +40,14 @@ script:
     export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m '
     set -ex
     sudo chown -R coq:coq /home/project
-    opam install coq-io-system -v --ignore-constraints-on=coq-io-system-ocaml
+    # Check if the package is compatible with the current environment
+    if opam install ${PACKAGE_NAME} --show-action; then
+      # First install the dependencies
+      opam install ${PACKAGE_NAME} --deps-only -y
+      opam list
+      # Then install the package itself in verbose mode
+      opam install ${PACKAGE_NAME} -v
+    fi;
     " script
 - docker stop COQ  # optional
 - echo -en 'travis_fold:end:script\\r'
diff --git a/coq-io-system-ocaml.opam b/coq-io-system-ocaml.opam
deleted file mode 100644
index 2c60872..0000000
--- a/coq-io-system-ocaml.opam
+++ /dev/null
@@ -1,25 +0,0 @@
-opam-version: "2.0"
-maintainer: "dev@clarus.me"
-homepage: "https://github.com/clarus/io-system"
-dev-repo: "git+https://github.com/clarus/io-system.git"
-bug-reports: "https://github.com/clarus/io-system/issues"
-authors: ["Guillaume Claret"]
-license: "MIT"
-build: [
-  [make "-C" "ocaml" "-j%{jobs}%"]
-]
-install: [
-  [make "-C" "ocaml" "install"]
-]
-depends: [
-  "lwt" {>= "2.4.7"}
-  "ocaml" {>= "4.00.0"}
-  "ocamlbuild"
-  "ocamlfind"
-  "num"
-]
-tags: [
-  "keyword:effects"
-  "keyword:extraction"
-]
-synopsis: "Extraction to OCaml of system effects"
diff --git a/coq-io-system.opam b/coq-io-system.opam
index fb666f9..1d8e657 100644
--- a/coq-io-system.opam
+++ b/coq-io-system.opam
@@ -18,7 +18,7 @@ depends: [
   "coq-function-ninjas"
   "coq-list-string" {>= "2.0.0"}
   "coq-io" {>= "4.0.0"}
-  "coq-io-system-ocaml" {= "2.5.0"}
+  "coq-io-system-ocaml" {>= "2.3.0"}
 ]
 tags: [
   "keyword:effects"
diff --git a/ocaml/.gitignore b/ocaml/.gitignore
deleted file mode 100644
index 69fa449..0000000
--- a/ocaml/.gitignore
+++ /dev/null
@@ -1 +0,0 @@
-_build/
diff --git a/ocaml/META b/ocaml/META
deleted file mode 100644
index 5d863e7..0000000
--- a/ocaml/META
+++ /dev/null
@@ -1,5 +0,0 @@
-description = "Coq system effects for extraction to OCaml."
-archive(byte) = "ioSystem.cma"
-archive(native) = "ioSystem.cmxa"
-version = "dev"
-requires = "lwt lwt.unix num"
diff --git a/ocaml/Makefile b/ocaml/Makefile
deleted file mode 100644
index 567a86b..0000000
--- a/ocaml/Makefile
+++ /dev/null
@@ -1,11 +0,0 @@
-default:
-	ocamlbuild ioSystem.cma ioSystem.cmxa -use-ocamlfind -package lwt,lwt.unix,num
-
-install: default
-	ocamlfind install io-system META _build/ioSystem.cmi _build/ioSystem.cmx _build/ioSystem.a _build/ioSystem.cma _build/ioSystem.cmxa _build/ioSystem.mllib
-
-uninstall:
-	ocamlfind remove io-system
-
-clean:
-	ocamlbuild -clean
diff --git a/ocaml/README.md b/ocaml/README.md
deleted file mode 100644
index 428ce1f..0000000
--- a/ocaml/README.md
+++ /dev/null
@@ -1,18 +0,0 @@
-# OCaml extraction
-> Utilities for extraction of system effects to [OCaml](http://ocaml.org/).
-
-This library is automatically included by the main `coq-io-system` package. It is also distributed as an independent opam package which does not depend on Coq. As a result, the compilation of extracted `.ml` files from programs with effects may not depend on Coq.
-
-## Install with opam
-Make sure you added the [Coq repository](http://coq.io/opam/):
-
-    opam repo add coq-released https://coq.inria.fr/opam/released
-
-and run:
-
-    opam install coq-io-system-ocaml
-
-## Install from source
-
-    make
-    make install
diff --git a/ocaml/ioSystem.ml b/ocaml/ioSystem.ml
deleted file mode 100644
index 997c126..0000000
--- a/ocaml/ioSystem.ml
+++ /dev/null
@@ -1,135 +0,0 @@
-(** Some OCaml primitives for the extraction. *)
-open Big_int
-
-(** Interface to OCaml's big integers. *)
-module Big = struct
-  let rec to_positive_aux (big : big_int) xH xO xI =
-    if eq_big_int big unit_big_int then
-      xH
-    else
-      let big' = to_positive_aux (div_big_int big (big_int_of_int 2)) xH xO xI in
-      if eq_big_int (mod_big_int big (big_int_of_int 2)) zero_big_int then
-        xO big'
-      else
-        xI big'
-
-  let to_Z_aux (big : big_int) z_O z_pos z_neg xH xO xI =
-    if eq_big_int big zero_big_int then
-      z_O
-    else if gt_big_int big zero_big_int then
-      z_pos (to_positive_aux big xH xO xI)
-    else
-      z_pos (to_positive_aux (minus_big_int big) xH xO xI)
-end
-
-(** Interface to the OCaml strings. *)
-module String = struct
-  (** Export an OCaml string. *)
-  let to_lstring (s : string) : char list =
-    let rec aux l i =
-      if i = -1 then
-        l
-      else
-        aux (s.[i] :: l) (i - 1) in
-    aux [] (String.length s - 1)
-
-  (** Import a Coq string. *)
-  let of_lstring (s : char list) : string =
-    let length = List.length s in
-    let buffer = Bytes.create length in
-    List.iteri (fun i c -> Bytes.set buffer i c) s;
-    Bytes.to_string buffer
-end
-
-(** The command line arguments of the program. *)
-let argv : string list =
-  Array.to_list Sys.argv
-
-(** Join. *)
-let join (x : 'a Lwt.t) (y : 'b Lwt.t) : ('a * 'b) Lwt.t =
-  let r_x = ref None in
-  let r_y = ref None in
-  Lwt.bind (Lwt.join [
-    Lwt.bind x (fun x -> r_x := Some x; Lwt.return ());
-    Lwt.bind y (fun y -> r_y := Some y; Lwt.return ())])
-    (fun (_ : unit) ->
-      match (!r_x, !r_y) with
-      | (Some x, Some y) -> Lwt.return (x, y)
-      | _ -> Lwt.fail_with "The join expected two answers.")
-
-(** Choose. *)
-let choose (x1 : 'a Lwt.t) (x2 : 'a Lwt.t) : 'a Lwt.t =
-  Lwt.pick [x1; x2]
-
-(** List the files of a directory. *)
-let list_files (directory : string) : string list option Lwt.t =
-  Lwt.catch (fun _ ->
-    let file_names = Lwt_unix.files_of_directory directory in
-    Lwt.bind (Lwt_stream.to_list file_names) (fun file_names ->
-    Lwt.return @@ Some file_names))
-    (fun _ -> Lwt.return None)
-
-(** Read the content of a file. *)
-let read_file (file_name : string) : string option Lwt.t =
-  Lwt.catch (fun _ ->
-    Lwt.bind (Lwt_io.open_file Lwt_io.Input file_name) (fun channel ->
-    Lwt.bind (Lwt_io.read channel) (fun content ->
-    Lwt.bind (Lwt_io.close channel) (fun _ ->
-    Lwt.return @@ Some content))))
-    (fun _ -> Lwt.return None)
-
-(** Update (or create) a file with some content. *)
-let write_file (file_name : string) (content : string) : bool Lwt.t =
-  Lwt.catch (fun _ ->
-    Lwt.bind (Lwt_io.open_file Lwt_io.Output file_name) (fun channel ->
-    Lwt.bind (Lwt_io.write channel content) (fun content ->
-    Lwt.bind (Lwt_io.close channel) (fun _ ->
-    Lwt.return true))))
-    (fun _ -> Lwt.return false)
-
-(** Delete a file. *)
-let delete_file (file_name : string) : bool Lwt.t =
-  Lwt.catch (fun _ ->
-    Lwt.bind (Lwt_unix.unlink file_name) (fun _ ->
-    Lwt.return true))
-    (fun _ -> Lwt.return false)
-
-(** Run a command. *)
-let system (command : string) : bool option Lwt.t =
-  Lwt.catch (fun _ ->
-    Lwt.bind (Lwt_unix.system command) (fun status ->
-    Lwt.return @@ Some (match status with
-    | Lwt_unix.WEXITED 0 | Lwt_unix.WSIGNALED 0 | Lwt_unix.WSTOPPED 0 -> true
-    | Lwt_unix.WEXITED _ | Lwt_unix.WSIGNALED _ | Lwt_unix.WSTOPPED _ -> false)))
-    (fun _ -> Lwt.return None)
-
-(** Run a command controlling the outputs. *)
-let eval (command : string list) : ((big_int * string) * string) option Lwt.t =
-  Lwt.catch (fun _ ->
-    let command = Array.of_list command in
-    Lwt_process.with_process_full ("", command) (fun process ->
-    Lwt.bind (process#status) (fun (status : Unix.process_status) ->
-    Lwt.bind (Lwt_io.read process#stdout) (fun (output : string) ->
-    Lwt.bind (Lwt_io.read process#stderr) (fun (error : string) ->
-    Lwt.bind (Lwt.join [
-      Lwt_io.close process#stdin;
-      Lwt_io.close process#stdout;
-      Lwt_io.close process#stderr]) (fun (_ : unit) ->
-    let status = match status with
-      | Unix.WEXITED n | Unix.WSIGNALED n | Unix.WSTOPPED n -> n in
-    Lwt.return @@ Some ((big_int_of_int status, output), error)))))))
-    (fun _ -> Lwt.return None)
-
-(** Print a message on the standard output. *)
-let print (message : string) : bool Lwt.t =
-  Lwt.catch (fun _ ->
-    Lwt.bind (Lwt_io.print message) (fun _ ->
-    Lwt.return true))
-    (fun _ -> Lwt.return false)
-
-(** Read a line on the standard input. *)
-let read_line () : string option Lwt.t =
-  Lwt.catch (fun _ ->
-    Lwt.bind (Lwt_io.read_line Lwt_io.stdin) (fun line ->
-    Lwt.return (Some line)))
-    (fun _ -> Lwt.return None)
diff --git a/ocaml/ioSystem.mllib b/ocaml/ioSystem.mllib
deleted file mode 100644
index b03ba1b..0000000
--- a/ocaml/ioSystem.mllib
+++ /dev/null
@@ -1 +0,0 @@
-IoSystem