From d4e6db77c5082e62a643f19105d6e7ee5547df29 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= <theo.zimmermann@inria.fr>
Date: Sat, 20 Aug 2022 12:56:18 +0200
Subject: [PATCH] Update for Coq 8.16 compatibility testing.

---
 .github/workflows/docker-action.yml |  1 +
 coq-corn.opam                       |  2 +-
 default.nix                         | 33 -----------------------------
 meta.yml                            |  3 ++-
 4 files changed, 4 insertions(+), 35 deletions(-)
 delete mode 100644 default.nix

diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 5d02a9f78..3f30c8584 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -18,6 +18,7 @@ jobs:
       matrix:
         image:
           - 'coqorg/coq:dev'
+          - 'coqorg/coq:8.16'
           - 'coqorg/coq:8.15'
           - 'coqorg/coq:8.14'
           - 'coqorg/coq:8.13'
diff --git a/coq-corn.opam b/coq-corn.opam
index be37b2ea9..fbbb7160c 100644
--- a/coq-corn.opam
+++ b/coq-corn.opam
@@ -46,7 +46,7 @@ build: [
 ]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.11" & < "8.16~") | (= "dev")}
+  "coq" {(>= "8.11" & < "8.17~") | (= "dev")}
   "coq-math-classes" {(>= "8.8.1") | (= "dev")}
   "coq-bignums" 
 ]
diff --git a/default.nix b/default.nix
deleted file mode 100644
index 45f680eae..000000000
--- a/default.nix
+++ /dev/null
@@ -1,33 +0,0 @@
-{ pkgs ? (import <nixpkgs> {}), coq-version-or-url, shell ? false }:
-
-let
-  coq-version-parts = builtins.match "([0-9]+).([0-9]+)" coq-version-or-url;
-  coqPackages =
-    if coq-version-parts == null then
-      pkgs.mkCoqPackages (import (fetchTarball coq-version-or-url) {})
-    else
-      pkgs."coqPackages_${builtins.concatStringsSep "_" coq-version-parts}";
-in
-
-let math-classes = coqPackages.math-classes.overrideAttrs (o: {
-    src = fetchTarball "https://github.com/coq-community/math-classes/archive/master.tar.gz";
-  }); in
-
-let inherit (coqPackages) coq bignums; in
-
-pkgs.stdenv.mkDerivation {
-
-  name = "corn";
-
-  propagatedBuildInputs = [
-    coq
-    math-classes
-    bignums
-  ];
-
-  src = if shell then null else ./.;
-
-  configurePhase = "sh ./configure.sh";
-
-  installFlags = "COQMF_COQLIB=$(out)/lib/coq/${coq.coq-version}/";
-}
diff --git a/meta.yml b/meta.yml
index 4fad1ef10..c9ee5dab6 100644
--- a/meta.yml
+++ b/meta.yml
@@ -80,10 +80,11 @@ license:
 
 supported_coq_versions:
   text: Coq 8.11 or greater
-  opam: '{(>= "8.11" & < "8.16~") | (= "dev")}'
+  opam: '{(>= "8.11" & < "8.17~") | (= "dev")}'
 
 tested_coq_opam_versions:
 - version: dev
+- version: "8.16"
 - version: "8.15"
 - version: "8.14"
 - version: "8.13"