From 10c2f692fb80280d76b684865189d0336825fc32 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 7 Feb 2017 11:34:45 +0100
Subject: [PATCH] Also support Coq 8.5pl3.

---
 Makefile            | 8 ++++++++
 README.md           | 4 ++--
 _CoqProject         | 1 -
 theories/fin_maps.v | 4 ++--
 theories/gmap.v     | 2 +-
 5 files changed, 13 insertions(+), 6 deletions(-)

diff --git a/Makefile b/Makefile
index 8de6ba8..1a7e330 100644
--- a/Makefile
+++ b/Makefile
@@ -3,6 +3,14 @@ ifeq ($(Y), 1)
 	YFLAG=-y
 endif
 
+# Determine Coq version
+COQ_VERSION=$(shell coqc --version | egrep -o 'version 8.[0-9]' | egrep -o '8.[0-9]')
+COQ_MAKEFILE_FLAGS ?=
+
+ifeq ($(COQ_VERSION), 8.6)
+	COQ_MAKEFILE_FLAGS += -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
+endif
+
 # Forward most targets to Coq makefile (with some trick to make this phony)
 %: Makefile.coq phony
 	+@make -f Makefile.coq $@
diff --git a/README.md b/README.md
index b04b95f..662a72a 100644
--- a/README.md
+++ b/README.md
@@ -20,7 +20,7 @@ The key features of this library are as follows:
   `set_solver` for goals involving set operations.
 - It is entirely axiom free.
 
-# History
+## History
 
 Coq-std++ has originally been developed by Robbert Krebbers as part of his
 formalization of the C programming language in his PhD thesis, called
@@ -32,7 +32,7 @@ developed by Robbert Krebbers, Ralf Jung, and Jacques Henri-Jourdan.
 
 This version is known to compile with:
 
- - Coq 8.6
+ - Coq 8.5pl3 and Coq 8.6
 
 ## Building Instructions
 
diff --git a/_CoqProject b/_CoqProject
index 8a0c466..a7869b1 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,5 +1,4 @@
 -Q theories stdpp
--arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
 theories/option.v
 theories/fin_map_dom.v
 theories/bset.v
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 7d0fab0..fe9d0f3 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -792,8 +792,8 @@ Section map_of_to_collection.
   Proof.
     intros Hinj. assert (∀ x',
       (i, x) ∈ f <$> elements Y → (i, x') ∈ f <$> elements Y → x = x').
-    { intros x'. intros (y&Hx&?%elem_of_elements)%elem_of_list_fmap.
-      intros (y'&Hx'&?%elem_of_elements)%elem_of_list_fmap.
+    { intros x'. intros (y&Hx&Hy)%elem_of_list_fmap (y'&Hx'&Hy')%elem_of_list_fmap.
+      rewrite elem_of_elements in Hy, Hy'.
       cut (y = y'); [congruence|]. apply Hinj; auto. by rewrite <-Hx, <-Hx'. }
     unfold map_of_collection; rewrite <-elem_of_map_of_list' by done.
     rewrite elem_of_list_fmap. setoid_rewrite elem_of_elements; naive_solver.
diff --git a/theories/gmap.v b/theories/gmap.v
index 1d988a6..97cc0af 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -130,7 +130,7 @@ Definition gmap_curry `{Countable K1, Countable K2} {A} :
     map_fold (λ i2 x, <[(i1,i2):=x]>) macc m') ∅.
 Definition gmap_uncurry `{Countable K1, Countable K2} {A} :
     gmap (K1 * K2) A → gmap K1 (gmap K2 A) :=
-  map_fold (λ '(i1,i2) x,
+  map_fold (λ ii x, let '(i1,i2) := ii in
     partial_alter (Some ∘ <[i2:=x]> ∘ from_option id ∅) i1) ∅.
 
 Section curry_uncurry.
-- 
GitLab