diff --git a/pkgs/applications/science/logic/coq/coq-8.3-make-3.82-compat.patch b/pkgs/applications/science/logic/coq/coq-8.3-make-3.82-compat.patch
new file mode 100644
index 00000000000..5176aa33ec8
--- /dev/null
+++ b/pkgs/applications/science/logic/coq/coq-8.3-make-3.82-compat.patch
@@ -0,0 +1,84 @@
+From: glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>
+Date: Tue, 19 Oct 2010 13:22:08 +0000 (+0000)
+Subject: Fix mixed implicit and normal rules
+X-Git-Url: https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq%2Fcoq-svn.git;a=commitdiff_plain;h=86eb08bad450dd3fa77b11e4a34d2f493ab80d85
+
+Fix mixed implicit and normal rules
+
+This fixes build with GNU Make 3.82. See threads:
+
+  https://sympa-roc.inria.fr/wws/arc/coqdev/2010-10/msg00025.html
+  http://thread.gmane.org/gmane.comp.gnu.make.bugs/4912
+
+git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.3@13566 85f007b7-540e-0410-9357-904b9bb8a0f7
+---
+
+diff --git a/Makefile b/Makefile
+index b1edc01..ea73c51 100644
+--- a/Makefile
++++ b/Makefile
+@@ -160,9 +160,19 @@ else
+ stage1 $(STAGE1_TARGETS) : always
+ 	$(call stage-template,1)
+ 
++ifneq (,$(STAGE1_IMPLICITS))
++$(STAGE1_IMPLICITS) : always
++	$(call stage-template,1)
++endif
++
+ stage2 $(STAGE2_TARGETS) : stage1
+ 	$(call stage-template,2)
+ 
++ifneq (,$(STAGE2_IMPLICITS))
++$(STAGE2_IMPLICITS) : stage1
++	$(call stage-template,2)
++endif
++
+ # Nota:
+ # - world is one of the targets in $(STAGE2_TARGETS), hence launching
+ # "make" or "make world" leads to recursion into stage1 then stage2
+diff --git a/Makefile.common b/Makefile.common
+index cc38980..46bf217 100644
+--- a/Makefile.common
++++ b/Makefile.common
+@@ -365,7 +365,7 @@ DATE=$(shell LANG=C date +"%B %Y")
+ 
+ SOURCEDOCDIR=dev/source-doc
+ 
+-CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot
++CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.o %.cmi %.cma %.cmxa %.a %.cmxs %.dep.ps %.dot
+ 
+ ### Targets forwarded by Makefile to a specific stage:
+ 
+@@ -374,10 +374,12 @@ CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot
+ STAGE1_TARGETS:= $(STAGE1) $(COQDEPBOOT) \
+   $(GENFILES) \
+   source-doc revision toplevel/mltop.byteml toplevel/mltop.optml \
+-  $(STAGE1_ML4:.ml4=.ml4-preprocessed) %.o
++  $(STAGE1_ML4:.ml4=.ml4-preprocessed)
++
++STAGE1_IMPLICITS:=
+ 
+ ifdef CM_STAGE1
+- STAGE1_TARGETS+=$(CAML_OBJECT_PATTERNS)
++ STAGE1_IMPLICITS+=$(CAML_OBJECT_PATTERNS)
+ endif
+ 
+ ## Enumeration of targets that require being done at stage2
+@@ -402,12 +404,13 @@ STAGE2_TARGETS:=$(COQBINARIES) lib kernel byterun library proofs tactics \
+   printers debug initplugins plugins \
+   world install coqide coqide-files coq coqlib \
+   coqlight states check init theories theories-light \
+-  $(DOC_TARGETS) $(VO_TARGETS) validate \
+-  %.vo %.glob states/% install-% %.ml4-preprocessed \
++  $(DOC_TARGETS) $(VO_TARGETS) validate
++
++STAGE2_IMPLICITS:= %.vo %.glob states/% install-% %.ml4-preprocessed \
+   $(DOC_TARGET_PATTERNS)
+ 
+ ifndef CM_STAGE1
+- STAGE2_TARGETS+=$(CAML_OBJECT_PATTERNS)
++ STAGE2_IMPLICITS+=$(CAML_OBJECT_PATTERNS)
+ endif
+ 
+ 
diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix
index d72a2104370..f63e03e9ad9 100644
--- a/pkgs/applications/science/logic/coq/default.nix
+++ b/pkgs/applications/science/logic/coq/default.nix
@@ -27,7 +27,7 @@ stdenv.mkDerivation {
 
   buildFlags = "world"; # Debug with "world VERBOSE=1";
 
-  patches = [ ./configure.patch ];
+  patches = [ ./configure.patch ./coq-8.3-make-3.82-compat.patch ];
 
   postPatch = ''
     UNAME=$(type -tp uname)