4 files changed, 24 insertions, 3 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 9737e1b2e0..cdf00f4767 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -31,7 +31,7 @@
 ########################################################################
 # Unicoq + Mtac2
 ########################################################################
-: "${unicoq_CI_REF:=68ed13294ea8860a8c39950f7ca2ff0aa7211b9f}"
+: "${unicoq_CI_REF:=master}"
 : "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq}"
 : "${unicoq_CI_ARCHIVEURL:=${unicoq_CI_GITURL}/archive}"
 
diff --git a/dev/ci/ci-unicoq.sh b/dev/ci/ci-unicoq.sh
index 36acb115e9..df1d9cceb8 100755
--- a/dev/ci/ci-unicoq.sh
+++ b/dev/ci/ci-unicoq.sh
@@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")"
 
 git_download unicoq
 
-( cd "${CI_BUILD_DIR}/unicoq" && coq_makefile -f Make -o Makefile && make && make install )
+( cd "${CI_BUILD_DIR}/unicoq" && coq_makefile -f _CoqProject -o Makefile && make && make install )
diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
index b3ced999f6..05624ff4a1 100644
--- a/dev/ci/nix/default.nix
+++ b/dev/ci/nix/default.nix
@@ -74,9 +74,20 @@ let Verdi = (coqPackages.Verdi.override { inherit Cheerios ssreflect; })
     src = fetchTarball "https://github.com/uwplse/verdi/tarball/master";
   }); in
 
+let flocq = coqPackages.flocq.overrideAttrs (o: {
+    src = fetchTarball "https://gitlab.inria.fr/flocq/flocq/-/archive/master/flocq-master.tar.gz";
+    configurePhase = ''
+      autoreconf
+      ${bash}/bin/bash configure --libdir=$out/lib/coq/${coq.coq-version}/user-contrib/Flocq
+    '';
+    buildPhase = ''
+      ./remake
+    '';
+  }); in
+
 let callPackage = newScope { inherit coq
   bignums coq-ext-lib coqprime corn iris math-classes
-  mathcomp simple-io ssreflect stdpp unicoq Verdi;
+  mathcomp simple-io ssreflect stdpp unicoq Verdi flocq;
 }; in
 
 # Environments for building CI libraries with this Coq
@@ -93,6 +104,7 @@ let projects = {
   fiat_crypto = callPackage ./fiat_crypto.nix {};
   flocq = callPackage ./flocq.nix {};
   formal-topology = callPackage ./formal-topology.nix {};
+  gappa = callPackage ./gappa.nix {};
   GeoCoq = callPackage ./GeoCoq.nix {};
   HoTT = callPackage ./HoTT.nix {};
   iris = callPackage ./iris.nix {};
diff --git a/dev/ci/nix/gappa.nix b/dev/ci/nix/gappa.nix
new file mode 100644
index 0000000000..8560cc072b
--- /dev/null
+++ b/dev/ci/nix/gappa.nix
@@ -0,0 +1,9 @@
+{ autoconf, automake, ocaml, flocq }:
+
+{
+  buildInputs = [ autoconf automake ocaml ];
+  coqBuildInputs = [ flocq ];
+  configure = "autoreconf && ./configure";
+  make = "./remake";
+  clean = "./remake clean";
+}