diff --git a/Makefile b/Makefile
index 8de6ba818504a6f83f508569ffd03a38689cab4c..1a7e330577c260f0a711cf623ca6413988a94165 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 b04b95f9f9ac614ad1da48e9f6131ef7e9665a72..662a72ac2c0832791fb98ddafe218dc77eedbe46 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 8a0c466a72688f6d95fcf9dd97d5553fba36cde6..a7869b1351ef752e6797dcbc94d5d18a0f6c1e7f 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 7d0fab06337adb791d8e20aa8b396dbff665ca02..fe9d0f36b3f0ed61c7ccb8e950f942edaf925381 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 1d988a62f80961fefec7e731ed7ac273a12dad91..97cc0afdaf57ef5acdbfdc60d41a1be746be6ab0 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.