From 06d597b68e2cdee65d486b2743870cea14cde4ab Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Jan 13 2017 04:56:40 +0000
Subject: New upstream release.


---

diff --git a/.gitignore b/.gitignore
index 74cfd33..fdc974e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -3,3 +3,4 @@
 /coq-8.5pl1.tar.gz
 /coq-8.5pl2.tar.gz
 /coq-8.5pl3.tar.gz
+/coq-8.6.tar.gz
diff --git a/coq-doc.patch b/coq-doc.patch
new file mode 100644
index 0000000..b3467bb
--- /dev/null
+++ b/coq-doc.patch
@@ -0,0 +1,14 @@
+Commit 42f27beb63a629dcef514abb0b31dea193f35a38: Fix incorrect documentation
+that prevents successful compilation (bug #5265).
+
+--- doc/refman/RefMan-syn.tex.orig	2016-12-08 08:13:52.000000000 -0700
++++ doc/refman/RefMan-syn.tex	2016-12-16 10:43:42.840463129 -0700
+@@ -649,7 +649,7 @@
+ pattern for terms. Here is an example:
+ 
+ \begin{coq_example*}
+-Notation ``'FUNAPP' x .. y , f'' :=
++Notation "'FUNAPP' x .. y , f" :=
+   (fun x => .. (fun y => (.. (f x) ..) y ) ..)
+   (at level 200, x binder, y binder, right associativity).
+ \end{coq_example*}
diff --git a/coq.spec b/coq.spec
index e733077..ec9ef5b 100644
--- a/coq.spec
+++ b/coq.spec
@@ -17,8 +17,8 @@
 # however, this name is proper as per the Coq documentation
 
 Name:           coq
-Version:        8.5pl3
-Release:        2%{?dist}
+Version:        8.6
+Release:        1%{?dist}
 Summary:        Proof management system
 
 License:        LGPLv2
@@ -29,8 +29,12 @@ Source2:        README.coq-emacs
 Source4:        coq.xml
 Source5:        coqide.appdata.xml
 
+# Upstream patch to fix a hung build while building documentation
+Patch0:         %{name}-doc.patch
+
 BuildRequires:  ocaml
 BuildRequires:  ocaml-camlp4-devel
+BuildRequires:  ocaml-findlib
 BuildRequires:  ocaml-lablgtk-devel
 BuildRequires:  csdp-tools
 BuildRequires:  desktop-file-utils
@@ -62,9 +66,9 @@ BuildRequires:  transfig
 Requires:       csdp-tools
 Requires:       texlive-base
 
-# Exclude a private ocaml interface that we don't Provide, and a Provides that
+# Exclude 2 private ocaml interfaces that we don't Provide, and a Provides that
 # the automatic generator is failing to produce for ocaml-lablgtk
-%global __requires_exclude ocaml\\\((Interface|GtkSourceView2_types)\\\)
+%global __requires_exclude ocaml\\\((Interface|Sos_types|GtkSourceView2_types)\\\)
 
 %description
 Coq is a formal proof management system. It allows for the development
@@ -117,20 +121,17 @@ Requires:       emacs(bin) >= %{_emacs_version}
 Requires:       emacs-proofgeneral
 BuildArch:      noarch
 
-# This can be removed when F-23 reaches EOL
-Obsoletes:      %{name}-emacs-el < 8.5-1%{?dist}
-Provides:       %{name}-emacs-el = %{version}-%{release}
-
 %description emacs
 This package provides GNU Emacs mode files for formatting Coq input.
 
 %prep
 %setup -q
+%patch0
 
 cp -p %SOURCE1 %SOURCE2 .
 
 # Fix a Makefile rule that causes installation to fail
-sed -ri '/FULLCONFIGDIR/s/OLDROOT|COQINSTALLPREFIX/&2/g' Makefile.build
+sed -ri '/FULLCONFIGDIR/s/OLDROOT|COQINSTALLPREFIX/&2/g' Makefile.install
 
 # Use relro due to network use.  Also fix broken CAML_LD_LIBRARY_PATH.
 sed -e 's/-lunix/& -ccopt -Wl,-z,relro/' \
@@ -209,7 +210,7 @@ cp -p doc/RecTutorial/RecTutorial.v %{buildroot}%{tutorialcodedir}
 ln -s %{tutorialcodedir} %{buildroot}%{coqdatadir}/RecTutorial
 
 # Install documentation not installed by install-doc in Makefile
-for f in CHANGES COMPATIBILITY CREDITS README;
+for f in CHANGES COMPATIBILITY CREDITS README.doc README.md;
 do cp -p $f %{buildroot}%{coqdocdir};
 done
 
@@ -247,7 +248,8 @@ mv ../*.el .
 %{coqdocdir}/CHANGES
 %{coqdocdir}/COMPATIBILITY
 %{coqdocdir}/CREDITS
-%{coqdocdir}/README
+%{coqdocdir}/README.doc
+%{coqdocdir}/README.md
 
 %files coqide
 %doc ide/FAQ
@@ -266,13 +268,17 @@ mv ../*.el .
 %exclude %{coqdocdir}/CHANGES
 %exclude %{coqdocdir}/COMPATIBILITY
 %exclude %{coqdocdir}/CREDITS
-%exclude %{coqdocdir}/README
+%exclude %{coqdocdir}/README.doc
+%exclude %{coqdocdir}/README.md
 
 %files emacs
 %doc README.coq-emacs
 %{_emacs_sitelispdir}/coq/
 
 %changelog
+* Thu Jan 12 2017 Jerry James <loganjerry@gmail.com> - 8.6-1
+- New upstream release
+
 * Sat Nov 05 2016 Richard W.M. Jones <rjones@redhat.com> - 8.5pl3-2
 - Rebuild for OCaml 4.04.0.
 
diff --git a/sources b/sources
index fdd6ee4..1ef3e59 100644
--- a/sources
+++ b/sources
@@ -1 +1 @@
-b1295e3ec6e27e301c1cb33de537b77d  coq-8.5pl3.tar.gz
+SHA512 (coq-8.6.tar.gz) = 9f5f4913fda8cf83683fec9398b42d4567207c3d4b52b4638d5e09a24ed25a43905fb57a9fac1bb9f9d681bd47f3560e1da74e79348b3a3fd93e2e8c686cebae