diff --git a/.github/workflows/proof_tools.yml b/.github/workflows/proof_tools.yml
index 82d47017026ae989c0c576a592fd1f7a8badbb55..2ac6f49c73d4de7fd49fc96f08fbffe314aebd10 100644
--- a/.github/workflows/proof_tools.yml
+++ b/.github/workflows/proof_tools.yml
@@ -8,7 +8,7 @@ jobs:
       fail-fast: false
       matrix:
         ocaml-compiler:
-          - 4.08.x
+          - 4.11.x
           - 4.13.x
 
     runs-on: ubuntu-latest
@@ -46,3 +46,10 @@ jobs:
         opam install . --deps-only --yes
         opam exec -- dune build
         opam exec -- dune runtest
+
+    - name: qfo
+      run: |
+        cd "${GITHUB_WORKSPACE}"/personoj/proofs/qfo || exit 1
+        opam install . --deps-only --yes
+        opam exec -- dune build
+        opam exec -- dune runtest
diff --git a/proofs/dune-exe.mk b/proofs/dune-exe.mk
index bc595aa522ec8fe1fd5a5762480baf9def0bcdcc..a7c746f57dae559e5bcb13deb37bc3155b053daf 100644
--- a/proofs/dune-exe.mk
+++ b/proofs/dune-exe.mk
@@ -16,6 +16,7 @@ psnj-${ROOT}: _build/default/${ROOT}.exe
 
 tests: _build/default/${ROOT}.exe
 	@${OPAM} exec -- ${DUNE} runtest
+	@echo 'Success'
 
 .if ${CMDLINER}
 ${EXE}.1: ${EXE}
diff --git a/proofs/qfo/Makefile b/proofs/qfo/Makefile
index 0dc23571f980e4539c71167cf031247f976ad7d4..2109686624aade8175a76833128fac444d9ed5a9 100644
--- a/proofs/qfo/Makefile
+++ b/proofs/qfo/Makefile
@@ -1,12 +1,11 @@
 PREFIX ?= /usr/local
-dune ?= dune
 
 _EXE = _build/default/bin/qfo.exe
 
 all: psnj-qfo psnj-qfo.1
 
 ${_EXE}:
-	@dune build
+	@opam exec dune build
 	
 psnj-qfo: ${_EXE}
 	@ln -sf ${_EXE} $@
@@ -24,6 +23,10 @@ uninstall:
 
 clean:
 	rm -f psnj-qfo psnj-qfo.1
-	dune clean
+	opam exec -- dune clean
 
-.PHONY: install uninstall clean
+tests:
+	@opam exec -- dune runtest
+	@echo 'Success'
+
+.PHONY: install uninstall clean tests
diff --git a/proofs/qfo/bin/qfo.ml b/proofs/qfo/bin/qfo.ml
index 24c4283d44a59711559a9961c370abeff910c469..625cb4bca467a6191fd9c65a411bf3e3cd2f39ff 100644
--- a/proofs/qfo/bin/qfo.ml
+++ b/proofs/qfo/bin/qfo.ml
@@ -51,7 +51,12 @@ let translate (lib_root : string option) (map_dir : (string * string) list)
   Library.set_lib_root lib_root;
   List.iter Library.add_mapping map_dir;
   Console.State.push ();
-  Package.apply_config (Sys.getcwd ());
+  (* Try to find lambdapi pkgs from current working directory, and do
+     nothing if it fails *)
+  try 
+    Package.apply_config (Sys.getcwd ());
+    Format.eprintf "Loaded package file from \"%s\"@." (Sys.getcwd ());
+  with Error.Fatal _ -> ();
   let mp = [ "<stdin>" ] in
   let sign = Sig_state.create_sign mp in
   let ss = Sig_state.of_sign sign in
@@ -132,8 +137,8 @@ let cmd =
     [
       `S Manpage.s_description
     ; `P
-        "$(tname) is a filter that transforms Dedukti files containing alist \
-         of axioms expressed in PVS-Cert into a list of axioms expressed in \
+        "$(tname) is a filter that transforms a list of Dedukti axioms \
+         encoded in PVS-Cert with dependent logical connectives into a list of axioms expressed in \
          something close to first order logic."
     ; `P
         "To convert files, the program needs identify the symbols of the \
diff --git a/proofs/qfo/dune-project b/proofs/qfo/dune-project
index 478cf895a24ca16f4599865459aceebc0d81181a..9c0c2402f98daf820f4edfd2205eb713fc3b0dd6 100644
--- a/proofs/qfo/dune-project
+++ b/proofs/qfo/dune-project
@@ -1,3 +1,11 @@
 (lang dune 2.9)
-(name lpvs)
+(name pvs_lp_qfo)
 (cram enable)
+
+(generate_opam_files true)
+(maintainers "dedukti-dev@inria.fr")
+
+(package
+ (name pvs_lp_qfo)
+ (synopsis "Transform PVS-Cert encoded lambdapi to solver friendly encodings")
+ (depends cmdliner yojson lambdapi))
diff --git a/proofs/qfo/lpvs.opam b/proofs/qfo/lpvs.opam
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/proofs/qfo/pvs_lp_qfo.opam b/proofs/qfo/pvs_lp_qfo.opam
new file mode 100644
index 0000000000000000000000000000000000000000..9e3543700b277f08ddb5af3dc9609786300c6a79
--- /dev/null
+++ b/proofs/qfo/pvs_lp_qfo.opam
@@ -0,0 +1,27 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "Transform PVS-Cert encoded lambdapi to solver friendly encodings"
+maintainer: ["dedukti-dev@inria.fr"]
+depends: [
+  "dune" {>= "2.9"}
+  "cmdliner"
+  "yojson"
+  "lambdapi"
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "--promote-install-files=false"
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+  ["dune" "install" "-p" name "--create-install-files" name]
+]