Merge remote-tracking branch 'origin/master' into stm+doc_hook

5 files changed, 12 insertions, 32 deletions

diff --git a/dev/ci/nix/bignums.nix b/dev/ci/nix/bignums.nix
index 1d931c858e..d813ddd8d7 100644
--- a/dev/ci/nix/bignums.nix
+++ b/dev/ci/nix/bignums.nix
@@ -1,5 +1,5 @@
 { ocamlPackages }:
 
 {
-  buildInputs = with ocamlPackages; [ ocaml findlib camlp5 ];
+  buildInputs = [ ocamlPackages.ocaml ];
 }
diff --git a/dev/ci/nix/coquelicot.nix b/dev/ci/nix/coquelicot.nix
new file mode 100644
index 0000000000..d379bfa73d
--- /dev/null
+++ b/dev/ci/nix/coquelicot.nix
@@ -0,0 +1,9 @@
+{ autoconf, automake, ssreflect }:
+
+{
+  buildInputs = [ autoconf automake ];
+  coqBuildInputs = [ ssreflect ];
+  configure = "./autogen.sh && ./configure";
+  make = "./remake";
+  clean = "./remake clean";
+}
diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
index 17070e66ee..a9cc91170f 100644
--- a/dev/ci/nix/default.nix
+++ b/dev/ci/nix/default.nix
@@ -72,6 +72,7 @@ let projects = {
   CoLoR = callPackage ./CoLoR.nix {};
   CompCert = callPackage ./CompCert.nix {};
   coq_dpdgraph = callPackage ./coq_dpdgraph.nix {};
+  coquelicot = callPackage ./coquelicot.nix {};
   Corn = callPackage ./Corn.nix {};
   cross_crypto = callPackage ./cross_crypto.nix {};
   Elpi = callPackage ./Elpi.nix {};
diff --git a/dev/ci/nix/flocq.nix b/dev/ci/nix/flocq.nix
index e153043557..71028ec2dc 100644
--- a/dev/ci/nix/flocq.nix
+++ b/dev/ci/nix/flocq.nix
@@ -4,4 +4,5 @@
   buildInputs = [ autoconf automake ];
   configure = "./autogen.sh && ./configure";
   make = "./remake";
+  clean = "./remake clean";
 }
diff --git a/dev/ci/nix/unicoq/unicoq-num.patch b/dev/ci/nix/unicoq/unicoq-num.patch
index 6d96d94dfc..6d2f6470b1 100644
--- a/dev/ci/nix/unicoq/unicoq-num.patch
+++ b/dev/ci/nix/unicoq/unicoq-num.patch
@@ -4,19 +4,6 @@ Date:   Thu Nov 29 08:59:22 2018 +0000
 
     Make explicit dependency to num
 
-diff --git a/Make b/Make
-index 550dc6a..8aa1309 100644
---- a/Make
-+++ b/Make
-@@ -9,7 +9,7 @@ src/logger.ml
- src/munify.mli
- src/munify.ml
- src/unitactics.mlg
--src/unicoq.mllib
-+src/unicoq.mlpack
- theories/Unicoq.v
- test-suite/munifytest.v
- test-suite/microtests.v
 diff --git a/Makefile.local b/Makefile.local
 new file mode 100644
 index 0000000..88be365
@@ -24,21 +11,3 @@ index 0000000..88be365
 +++ b/Makefile.local
 @@ -0,0 +1 @@
 +CAMLPKGS += -package num
-diff --git a/src/unicoq.mllib b/src/unicoq.mllib
-deleted file mode 100644
-index 2b84e2d..0000000
---- a/src/unicoq.mllib
-+++ /dev/null
-@@ -1,3 +0,0 @@
--Logger
--Munify
--Unitactics
-diff --git a/src/unicoq.mlpack b/src/unicoq.mlpack
-new file mode 100644
-index 0000000..2b84e2d
---- /dev/null
-+++ b/src/unicoq.mlpack
-@@ -0,0 +1,3 @@
-+Logger
-+Munify
-+Unitactics