Merge pull request #60 from coq-community/refresh-from-templates

Coq 8.12 compatibility
coq-community · Aug 12, 2020 · 6cd1577 · 6cd1577
2 parents 9f74a7b + e576536
commit 6cd1577
Show file tree

Hide file tree

Showing 6 changed files with 12 additions and 13 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -4,8 +4,13 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 ## [Unreleased]
+
+## [8.12.0] - 2020-08-12
 ### Added
 - Support for building with dune
+### Fixed
+- Coq 8.12 compatibility
+- `notation-incompatible-format` warning suppression to build with Coq 8.12
 
 ## [8.11.0] - 2020-02-01
 ### Removed

diff --git a/README.md b/README.md
@@ -41,6 +41,7 @@ re-implementations for comparison.
   - Beta Ziliani (initial)
   - Aleksandar Nanevski (initial)
   - Derek Dreyer (initial)
+
 - Coq-community maintainer(s):
   - Anton Trunov ([**@anton-trunov**](https://github.com/anton-trunov))
 - License: [GNU General Public License v3.0 or later](LICENSE.md)

diff --git a/_CoqProject b/_CoqProject
@@ -4,6 +4,7 @@
 -arg -w -arg -notation-overridden
 -arg -w -arg -projection-no-head-constant
 -arg -w -arg -redundant-canonical-projection
+-arg -w -arg -notation-incompatible-format
 
 theories/prelude.v
 theories/rels.v

diff --git a/default.nix b/default.nix
@@ -11,15 +11,6 @@ in
 
 with coqPackages;
 
-let
-  ssreflect =
-    coqPackages.ssreflect.overrideAttrs(_: rec {
-      name = "coq-${coq.coq-version}-ssreflect-${version}";
-      version = "dev";
-      src = fetchTarball "https://github.com/math-comp/math-comp/tarball/master";
-    });
-in
-
 pkgs.stdenv.mkDerivation {
 
   name = "lemma-overloading";

diff --git a/dune-project b/dune-project
@@ -1,3 +1,3 @@
-(lang dune 2.3)
-(using coq 0.1)
-(name coq-lemma-overloading)
+(lang dune 2.5)
+(using coq 0.2)
+(name lemma-overloading)
diff --git a/theories/dune b/theories/dune
@@ -6,4 +6,5 @@
    -w +default
    -w -notation-overridden
    -w -projection-no-head-constant
-   -w -redundant-canonical-projection))
+   -w -redundant-canonical-projection
+   -w -notation-incompatible-format))