[why] Add -coq84 patches to adapt to Coq 8.4. Cripple the Jessie plugin until problems with frama-c and ha

[Jerry James]

commit b732eff318a5e5f302c30158966facb7d253fa82
Author: Jerry James <jamesjer at betterlinux.com>
Date:   Thu Aug 23 14:53:21 2012 -0600

    Add -coq84 patches to adapt to Coq 8.4.
    Cripple the Jessie plugin until problems with frama-c and hashtables are fixed.

 why-2.31-coq84.patch |   16 ++++++++++++++++
 why.spec             |   17 +++++++++++------
 2 files changed, 27 insertions(+), 6 deletions(-)
---
diff --git a/why-2.31-coq84.patch b/why-2.31-coq84.patch
new file mode 100644
index 0000000..cff6767
--- /dev/null
+++ b/why-2.31-coq84.patch
@@ -0,0 +1,16 @@
+--- ./lib/coq/WhyTuples.v.orig	2012-07-19 12:33:10.000000000 -0600
++++ ./lib/coq/WhyTuples.v	2012-08-23 11:58:18.246520358 -0600
+@@ -20,11 +20,9 @@
+ 
+ Definition tuple_1 (X:Set) := X.
+ 
+-Definition tuple_2 := prod.
+-Definition Build_tuple_2 := pair.
++Record tuple_2 (T1 T2:Set) : Set :=
++  {proj_2_1 : T1; proj_2_2 : T2}.
+ Implicit Arguments Build_tuple_2.
+-Definition proj_2_1 := fst.
+-Definition proj_2_2 := snd.
+ 
+ Record tuple_3 (T1 T2 T3:Set) : Set := 
+   {proj_3_1 : T1; proj_3_2 : T2; proj_3_3 : T3}.
diff --git a/why.spec b/why.spec
index e778737..c964198 100644
--- a/why.spec
+++ b/why.spec
@@ -60,11 +60,14 @@ Patch2:         %{name}-2.31-warning.patch
 # Adapt to changes in OCaml 4.00.0.
 Patch3:         %{name}-2.31-ocaml4.patch
 
+# Adapt to changes in coq 8.4.
+Patch4:         %{name}-2.31-coq84.patch
+
 BuildRequires:  auto-destdir
 BuildRequires:  cvc3
 BuildRequires:  desktop-file-utils
 BuildRequires:  emacs-nox xemacs xemacs-packages-extra
-BuildRequires:  frama-c-devel
+#BuildRequires:  frama-c-devel
 BuildRequires:  gappalib-coq
 BuildRequires:  gtk2-devel
 BuildRequires:  ocaml
@@ -221,6 +224,7 @@ based on Why, including various automated and interactive provers.
 %patch1
 %patch2
 %patch3
+%patch4
 
 cp -p %SOURCE1 %SOURCE2 %SOURCE6 %SOURCE7 ./
 
@@ -276,7 +280,7 @@ sed -e 's/\(versions_ok = \["0\.13\.0";"0\.14\.0";"0\.15\.1"\)\];/\1;"0.16.0";"0
     -e 's/versions_ok = \["0\.93"\]/versions_ok = ["0.93";"0.94"]/' \
     -e 's/versions_ok = \["1\.0\.25";.*\]/versions_ok = ["1.0.35"]/' \
     -e 's/versions_ok = \["2.2"\]/versions_ok = ["2.4.1"]/' \
-    -e 's/versions_ok = \["8\.0";.*\]/versions_ok = ["8.3pl4"]/' \
+    -e 's/versions_ok = \["8\.0";.*\]/versions_ok = ["8.4"]/' \
     -e 's/versions_ok = \["4\.1"\]/versions_ok = ["5.0"]/' \
     -e 's/command = "pvs"/command = "pvs-sbcl"/' \
     -e 's/PVS, (pvs, \["pvs"\]);/PVS, (pvs, ["pvs-sbcl" ; "pvs"]);/' \
@@ -292,7 +296,7 @@ make %{opt_option}
 
 # Strip binaries (the Makefile misses some of them)
 strip bin/why-cpulimit
-strip frama-c-plugin/Jessie.cmxs
+#strip frama-c-plugin/Jessie.cmxs
 %if %opt
 strip bin/rv_merge.opt bin/simplify2why.opt bin/tool-stat.opt \
       bin/why2html.opt bin/why-dp.opt bin/why-obfuscator.opt bin/why-stat.opt
@@ -407,7 +411,7 @@ diff -u min.why min_why.why.result  # Show differences from correct result.
 %files jessie
 %{_bindir}/jessie
 %{_libdir}/jessie/
-%{_libdir}/frama-c/plugins/Jessie.*
+#%%{_libdir}/frama-c/plugins/Jessie.*
 %{_datadir}/applications/fedora-jessie.desktop
 
 %if %{has_coq}
@@ -440,11 +444,12 @@ diff -u min.why min_why.why.result  # Show differences from correct result.
 
 
 %changelog
-* Mon Jul 30 2012 Jerry James <loganjerry at gmail.com> - 2.31-1
+* Thu Aug 23 2012 Jerry James <loganjerry at gmail.com> - 2.31-1
 - New upstream version
 - Drop upstreamed patches
 - Add ocaml-mlgmpidl-devel and why3 BRs
-- Add -warning and -ocaml4 patches to fix the build
+- Add -warning, -ocaml4, and -coq84 patches to fix the build
+- Cripple the Jessie plugin until problems with frama-c and hashtables are fixed
 
 * Mon Jul 30 2012 Richard W.M. Jones <rjones at redhat.com> - 2.30-7
 - Rebuild for OCaml 4.00.0 official.