[why3] Add patch to adapt to coq 8.4.

[Jerry James]

commit f753d82a9a1912d49191cb7aa452a94b11ee6c5b
Author: Jerry James <jamesjer at betterlinux.com>
Date:   Thu Aug 23 14:09:13 2012 -0600

    Add patch to adapt to coq 8.4.

 why3-coq84.patch |   67 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 why3.spec        |    3 ++
 2 files changed, 70 insertions(+), 0 deletions(-)
---
diff --git a/why3-coq84.patch b/why3-coq84.patch
new file mode 100644
index 0000000..19a5980
--- /dev/null
+++ b/why3-coq84.patch
@@ -0,0 +1,67 @@
+--- ./src/coq-tactic/why3tac.ml.orig	2012-07-19 06:05:03.000000000 -0600
++++ ./src/coq-tactic/why3tac.ml	2012-08-23 13:57:51.993724381 -0600
+@@ -473,7 +473,7 @@ and tr_global_ts dep env r =
+           let (_,vars), _, t = decomp_type_quantifiers env ty in
+           if not (is_Set t) && not (is_Type t) then raise NotFO;
+           let id = preid_of_id (Nametab.basename_of_global r) in
+-          let ts = match (Global.lookup_constant c).const_body with
++          let ts = match (body_of_constant (Global.lookup_constant c)) with
+             | Some b ->
+                 let b = force b in
+                 let tvm, env, t = decomp_type_lambdas Idmap.empty env vars b in
+@@ -621,7 +621,7 @@ and make_one_ls dep env r =
+   add_poly_arity ls vars
+ 
+ and decompose_definition dep env c =
+-  let dl = match (Global.lookup_constant c).const_body with
++  let dl = match (body_of_constant (Global.lookup_constant c)) with
+     | None ->
+         [ConstRef c, None]
+     | Some b ->
+@@ -1091,8 +1091,6 @@ let tr_top_decl = function
+   | _, Lib.CompilingLibrary _
+   | _, Lib.OpenedModule _
+   | _, Lib.ClosedModule  _
+-  | _, Lib.OpenedModtype _
+-  | _, Lib.ClosedModtype _
+   | _, Lib.OpenedSection _
+   | _, Lib.ClosedSection _
+   | _, Lib.FrozenState _ -> ()
+--- ./src/coq-tactic/g_why3tac.ml.orig	2012-07-19 06:05:03.000000000 -0600
++++ ./src/coq-tactic/g_why3tac.ml	2012-08-23 13:59:15.218727554 -0600
+@@ -47,20 +47,20 @@ let _ =
+               (Util.dummy_loc,
+                Tacexpr.TacExtend (Util.dummy_loc, "Why3", l))))
+       []
+-  with e -> Pp.pp (Cerrors.explain_exn e)
++  with e -> Pp.pp (Errors.print e)
+ let _ =
+   Egrammar.extend_tactic_grammar "Why3"
+     [[Egrammar.GramTerminal "why3";
+       Egrammar.GramNonTerminal
+         (Util.dummy_loc, Genarg.StringArgType,
+-         Extend.Aentry ("prim", "string"), Some (Names.id_of_string "s"))];
++         Pcoq.Aentry ("prim", "string"), Some (Names.id_of_string "s"))];
+      [Egrammar.GramTerminal "why3";
+       Egrammar.GramNonTerminal
+         (Util.dummy_loc, Genarg.StringArgType,
+-         Extend.Aentry ("prim", "string"), Some (Names.id_of_string "s"));
++         Pcoq.Aentry ("prim", "string"), Some (Names.id_of_string "s"));
+       Egrammar.GramTerminal "timelimit";
+       Egrammar.GramNonTerminal
+-        (Util.dummy_loc, Genarg.IntArgType, Extend.Aentry ("prim", "integer"),
++        (Util.dummy_loc, Genarg.IntArgType, Pcoq.Aentry ("prim", "integer"),
+          Some (Names.id_of_string "n"))]]
+ let _ =
+   List.iter Pptactic.declare_extra_tactic_pprule
+--- ./lib/coq/int/Int.v.orig	2012-07-19 06:05:03.000000000 -0600
++++ ./lib/coq/int/Int.v	2012-08-23 13:57:52.000724506 -0600
+@@ -13,7 +13,7 @@ Lemma infix_lseq_Zle :
+   forall x y, infix_lseq x y <-> Zle x y.
+ Proof.
+ intros x y.
+-apply iff_Symmetric.
++apply RelationClasses.iff_Symmetric.
+ apply Zle_lt_or_eq_iff.
+ Qed.
+ 
diff --git a/why3.spec b/why3.spec
index 441d103..7e4a011 100644
--- a/why3.spec
+++ b/why3.spec
@@ -14,6 +14,8 @@ Source0:        https://gforge.inria.fr/frs/download.php/31257/%{name}-%{version
 # Man pages written by Jerry James using text found in the sources.  Hence,
 # the copyright and license are the same as for the upstream sources.
 Source1:        %{name}-man.tar.xz
+# Adapt to coq 8.4.
+Patch0:         %{name}-coq84.patch
 
 BuildRequires:  coq
 BuildRequires:  evince
@@ -99,6 +101,7 @@ based on Why3, including various automated and interactive provers.
 %prep
 %setup -q
 %setup -q -T -D -a 1
+%patch0
 
 # Use the correct compiler flags, fix PVS realizations, and keep timestamps
 sed -e "s|-Wall|$RPM_OPT_FLAGS|" \