diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..3c891f7
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,2 @@
+/krakatoa.pdf
+/why-2.30.tar.gz
diff --git a/README.why b/README.why
new file mode 100644
index 0000000..ba95dfa
--- /dev/null
+++ b/README.why
@@ -0,0 +1,8 @@
+Fedora why package:
+
+Contains the main why executable and supporting tools.
+
+Consider visiting the main Why site - http://why.lri.fr - for more
+documentation. Also, there is more information about the tools
+Caduceus and Krakatoa at http://caduceus.lri.fr and
+http://krakatoa.lri.fr respectively.
\ No newline at end of file
diff --git a/README.why-coq.Fedora b/README.why-coq.Fedora
new file mode 100644
index 0000000..406a7a9
--- /dev/null
+++ b/README.why-coq.Fedora
@@ -0,0 +1,6 @@
+Fedora why-coq package:
+
+Contains libraries for interfacing why with Coq.
+
+You shouldn't have to do anything extra - you should now just be able
+to use the Coq-related capabilities of Why.
\ No newline at end of file
diff --git a/README.why-gwhy.Fedora b/README.why-gwhy.Fedora
new file mode 100644
index 0000000..3cc41b4
--- /dev/null
+++ b/README.why-gwhy.Fedora
@@ -0,0 +1,6 @@
+Fedora why-gwhy package:
+
+Contains the gwhy GUI for Why.
+
+Run gwhy with "gwhy <filename>". (If you forget and run without a
+filename you'll be prompted for it.)
\ No newline at end of file
diff --git a/dead.package b/dead.package
deleted file mode 100644
index 497866a..0000000
--- a/dead.package
+++ /dev/null
@@ -1 +0,0 @@
-Abandoned by upstream and fails to build from source
diff --git a/div.pvs b/div.pvs
new file mode 100644
index 0000000..4005fe3
--- /dev/null
+++ b/div.pvs
@@ -0,0 +1,35 @@
+% Copyright (c) 2010 Jerry James.
+% 
+% Permission is hereby granted, free of charge, to any person obtaining a copy
+% of this software and associated documentation files (the "Software"), to deal
+% in the Software without restriction, including without limitation the rights
+% to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+% copies of the Software, and to permit persons to whom the Software is
+% furnished to do so, subject to the following conditions:
+% 
+% The above copyright notice and this permission notice shall be included in
+% all copies or substantial portions of the Software.
+% 
+% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+% IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+% FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+% AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+% LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+% OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+% THE SOFTWARE.
+
+div: THEORY
+BEGIN
+
+  x   : VAR int
+  nzy : VAR nzint
+
+  div(x, nzy): int =
+  IF (x >= 0 AND nzy > 0) THEN ndiv(x, nzy)
+  ELSIF (x >= 0 AND nzy < 0) THEN -ndiv(x, -nzy)
+  ELSIF (x < 0 AND nzy > 0) THEN -ndiv(-x, nzy)
+  ELSE ndiv(-x, -nzy)
+  ENDIF
+
+END div
+
diff --git a/gwhy-2.26.patch b/gwhy-2.26.patch
new file mode 100644
index 0000000..15a2576
--- /dev/null
+++ b/gwhy-2.26.patch
@@ -0,0 +1,53 @@
+--- bin/gwhy.sh.orig	2011-03-02 01:27:41.000000000 -0700
++++ bin/gwhy.sh	2011-07-07 15:41:07.232455718 -0600
+@@ -1,11 +1,17 @@
+ #!/bin/sh
+ 
+-case $1 in
++if ! test $1; then
++file=`zenity --file-selection --title="Select the file you want to open with gwhy"`;
++else
++file=$1
++fi
++
++case $file in
+   *.java)
+-	b=`basename $1 .java`
+-	krakatoa $1 || exit 1
++	b=`basename $file .java`
++	krakatoa $file || exit 1
+ 	echo "krakatoa on $b.java done"
+-        d=`dirname $1`
++        d=`dirname $file`
+         echo "cd $d"
+         cd $d
+ 	jessie -locs $b.jloc -why-opt -split-user-conj $b.jc || exit 2
+@@ -13,20 +19,23 @@
+ 	make -f $b.makefile gui
+ 	;;
+   *.c)
+-	b=`basename $1 .c`
+-	caduceus -why-opt -split-user-conj $1 || exit 1
++	b=`basename $file .c`
++	caduceus -why-opt -split-user-conj $b.c || exit 1
+ 	make -f $b.makefile gui
+ 	;;
+   *.jc)
+-	b=`basename $1 .jc`
++	b=`basename $file .jc`
+ 	jessie -why-opt -split-user-conj $b.jc || exit 1
+ 	make -f $b.makefile gui
+ 	;;
+   *.mlw|*.why)
+-	gwhy-bin -split-user-conj $1
++	gwhy-bin -split-user-conj $file
++	;;
++  ?*)
++	echo "$file does not have file type extension recognized by gwhy"
+ 	;;
+   *)
+-	echo "don't know what to do with $1"
++	echo "gwhy needs the name of a file to inspect in order to run"
+ esac
+ 
+ 
diff --git a/gwhy-icon.png b/gwhy-icon.png
new file mode 100644
index 0000000..9a1b76c
Binary files /dev/null and b/gwhy-icon.png differ
diff --git a/gwhy.desktop b/gwhy.desktop
new file mode 100644
index 0000000..27f853a
--- /dev/null
+++ b/gwhy.desktop
@@ -0,0 +1,8 @@
+[Desktop Entry]
+Encoding=UTF-8
+Name=gwhy
+Comment=Examine and develop Why .why files
+Exec=gwhy
+Icon=ICON-LOCATION-BASE/gwhy-icon.png
+Type=Application
+Categories=Development;
\ No newline at end of file
diff --git a/jessie.desktop b/jessie.desktop
new file mode 100644
index 0000000..239f37a
--- /dev/null
+++ b/jessie.desktop
@@ -0,0 +1,8 @@
+[Desktop Entry]
+Encoding=UTF-8
+Name=jessie
+Comment=Verify C program using Jessie plug-in
+Exec=frama-c -jessie %f
+Icon=ICON-LOCATION-BASE/gwhy-icon.png
+Type=Application
+Categories=Development;
diff --git a/min.mlw b/min.mlw
new file mode 100644
index 0000000..ae72dea
--- /dev/null
+++ b/min.mlw
@@ -0,0 +1,4 @@
+logic min: int, int -> int
+axiom min_ax: forall x,y:int. min(x,y) <= x
+parameter r: int ref
+let f (n:int) = {} r := min !r n { r <= r@ }
\ No newline at end of file
diff --git a/min_why.why.result b/min_why.why.result
new file mode 100644
index 0000000..04848f9
--- /dev/null
+++ b/min_why.why.result
@@ -0,0 +1,41 @@
+logic eq_unit : unit, unit -> prop
+
+logic neq_unit : unit, unit -> prop
+
+logic eq_bool : bool, bool -> prop
+
+logic neq_bool : bool, bool -> prop
+
+logic lt_int : int, int -> prop
+
+logic le_int : int, int -> prop
+
+logic gt_int : int, int -> prop
+
+logic ge_int : int, int -> prop
+
+logic eq_int : int, int -> prop
+
+logic neq_int : int, int -> prop
+
+logic add_int : int, int -> int
+
+logic sub_int : int, int -> int
+
+logic mul_int : int, int -> int
+
+logic neg_int : int -> int
+
+predicate zwf_zero(a: int, b: int) = ((0 <= b) and (a < b))
+
+logic min : int, int -> int
+
+axiom min_ax: (forall x:int. (forall y:int. (min(x, y) <= x)))
+
+goal f_po_1:
+  forall n:int.
+  forall r0:int.
+  forall r:int.
+  (r = min(r0, n)) ->
+  (r <= r0)
+
diff --git a/patch_jessie_pvs b/patch_jessie_pvs
new file mode 100755
index 0000000..3e4abca
--- /dev/null
+++ b/patch_jessie_pvs
@@ -0,0 +1,59 @@
+#!/bin/sh
+
+# To use PVS with frama-c without the NASA Langley PVS library:
+#   frama-c -jessie -jessie-atp pvs FILE.c  # Generates PVS files
+#   cd FILE.jessie/pvs
+#   patch_jessie_pvs # Patch jessie_why.pvs to not need NASA Langley library.
+# You can then run PVS to prove the generated theorems with:
+#   pvs-sbcl FILE_why.pvs
+#
+# Copyright (c) 2010 David A. Wheeler
+# 
+# Permission is hereby granted, free of charge, to any person obtaining a copy
+# of this software and associated documentation files (the "Software"), to deal
+# in the Software without restriction, including without limitation the rights
+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+# copies of the Software, and to permit persons to whom the Software is
+# furnished to do so, subject to the following conditions:
+# 
+# The above copyright notice and this permission notice shall be included in
+# all copies or substantial portions of the Software.
+# 
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+# THE SOFTWARE.
+
+
+if [ ! -f jessie_why.pvs ] ; then
+  echo "Did not find file jessie_why.pvs in current directory"
+  exit 1
+fi
+
+patch -p0 -N << END_OF_PATCH
+--- jessie_why.pvs.ORIGINAL	2010-10-05 14:41:58.965970651 -0400
++++ jessie_why.pvs	2010-10-06 14:28:39.250971269 -0400
+@@ -169,14 +169,14 @@
+     (FORALL (x: real): (FORALL (y: real): min(x, y) = x OR min(x, y) = y))
+ 
+   %% Why axiom sqrt_pos
+-  sqrt_pos: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES sqrt(x) >= 0.0))
++  % sqrt_pos: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES sqrt(x) >= 0.0))
+ 
+   %% Why axiom sqrt_sqr
+-  sqrt_sqr: AXIOM
+-    (FORALL (x: real): (x >= 0.0 IMPLIES sqr_real(sqrt(x)) = x))
++  % sqrt_sqr: AXIOM
++  %  (FORALL (x: real): (x >= 0.0 IMPLIES sqr_real(sqrt(x)) = x))
+ 
+   %% Why axiom sqr_sqrt
+-  sqr_sqrt: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES sqrt(x * x) = x))
++  % sqr_sqrt: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES sqrt(x * x) = x))
+ 
+   %% Why axiom abs_real_pos
+   abs_real_pos: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES abs(x) = x))
+END_OF_PATCH
+
diff --git a/rem.pvs b/rem.pvs
new file mode 100644
index 0000000..4f126a6
--- /dev/null
+++ b/rem.pvs
@@ -0,0 +1,35 @@
+% Copyright (c) 2010 Jerry James.
+%
+% Permission is hereby granted, free of charge, to any person obtaining a copy
+% of this software and associated documentation files (the "Software"), to deal
+% in the Software without restriction, including without limitation the rights
+% to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+% copies of the Software, and to permit persons to whom the Software is
+% furnished to do so, subject to the following conditions:
+%
+% The above copyright notice and this permission notice shall be included in
+% all copies or substantial portions of the Software.
+%
+% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+% IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+% FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+% AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+% LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+% OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+% THE SOFTWARE.
+
+rem: THEORY
+BEGIN
+
+  x   : VAR int
+  nzy : VAR nzint
+
+  rem(x, nzy): int =
+  IF (x >= 0 AND nzy > 0) THEN rem(nzy)(x)
+  ELSIF (x >= 0 AND nzy < 0) THEN rem(-nzy)(x)
+  ELSIF (x < 0 AND nzy > 0) THEN -rem(nzy)(-x)
+  ELSE -rem(-nzy)(-x)
+  ENDIF
+
+END rem
+
diff --git a/sources b/sources
new file mode 100644
index 0000000..ae20770
--- /dev/null
+++ b/sources
@@ -0,0 +1,2 @@
+1e8d6c76e5c3cee018172e981309c68b  krakatoa.pdf
+c3f6c5616e32743e883ffb7609f96336  why-2.30.tar.gz
diff --git a/why-2.30-Makefile.in.patch b/why-2.30-Makefile.in.patch
new file mode 100644
index 0000000..eb43de5
--- /dev/null
+++ b/why-2.30-Makefile.in.patch
@@ -0,0 +1,20 @@
+--- Makefile.in.orig	2011-10-24 09:21:06.000000000 -0600
++++ Makefile.in	2011-10-25 15:37:54.600278865 -0600
+@@ -782,14 +782,9 @@
+ 	cp -f $(V7FILES) $(LIBDIR)/why/coq7
+ 	cp -f $(VO7) $(LIBDIR)/why/coq7
+ install-coq-v8 install-coq-v8.1:
+-	if test -w $(COQLIB) ; then \
+-	  mkdir -p $(COQLIB)/user-contrib/Why ; \
+-	  cp -f $(VO8) $(COQLIB)/user-contrib/Why ; \
+-	else \
+-	  echo "Cannot copy to Coq standard library. Add \"-R $(LIBDIR)/why/coq Why\" to Coq options." ;\
+-	mkdir -p $(LIBDIR)/why/coq ;\
+-	cp -f $(VO8) $(V8FILES) $(LIBDIR)/why/coq ;\
+-	fi
++	mkdir -p $(COQLIB)/user-contrib/Why
++	cp -f $(V8FILES) $(COQLIB)/user-contrib/Why
++	cp -f $(VO8) $(COQLIB)/user-contrib/Why
+ 
+ install-pvs-no:
+ install-pvs-yes: $(PVSFILES)
diff --git a/why-apron.patch b/why-apron.patch
new file mode 100644
index 0000000..4e23767
--- /dev/null
+++ b/why-apron.patch
@@ -0,0 +1,40 @@
+--- jc/jc_annot_inference.ml.orig	2011-10-24 09:21:06.000000000 -0600
++++ jc/jc_annot_inference.ml	2011-11-23 13:47:40.438177237 -0700
+@@ -148,7 +148,7 @@
+ 	      Some(tptr,offt)
+ 	end
+     | JCTvar _ | JCTderef _ | JCTapp _ | JCTold _ | JCTat _ | JCTif _ 
+-    | JCTrange _ | JCTmatch _ | JCTaddress _ | JCTbase_block _
++    | JCTlet _ | JCTrange _ | JCTmatch _ | JCTaddress _ | JCTbase_block _
+     | JCTconst _ | JCTbinary _ | JCTunary _ | JCToffset _ | JCTinstanceof _ 
+     | JCTreal_cast _ | JCTrange_cast _ | JCTbitwise_cast _ | JCTcast _ ->
+ 	None
+@@ -491,7 +491,7 @@
+   in
+   Format.fprintf Format.str_formatter "%a" Jc_output.assertion a;
+   let formula = Format.flush_str_formatter () in
+-  let lab = Output.reg_pos "G" ?id ?kind ?name ~formula loc in
++  let lab = Output.old_reg_pos "G" ?id ?kind ?name ~formula (Loc.extract loc) in
+   new assertion_with ~mark:lab a
+ 
+ 
+@@ -608,8 +608,8 @@
+ 	Atp.Fn(atp_of_unop uop, [atp_of_term t1])
+     | JCTvar _ | JCTderef _ | JCTapp _ | JCToffset _ ->
+ 	Atp.Var (Vwp.variable_for_term t)
+-    | JCTshift _ | JCTold _ | JCTat _ | JCTmatch _ | JCTinstanceof _ 
+-    | JCTcast _ | JCTrange_cast _ | JCTbitwise_cast _ | JCTreal_cast _ 
++    | JCTshift _ | JCTold _ | JCTat _ | JCTmatch _ | JCTinstanceof _ | JCTlet _
++    | JCTcast _ | JCTrange_cast _ | JCTbitwise_cast _ | JCTreal_cast _
+     | JCTaddress _ | JCTif _ | JCTrange _ | JCTunary _ | JCTbase_block _ ->
+ 	err ()
+ 
+@@ -1198,7 +1198,7 @@
+       | JCTunary _ | JCTshift _ | JCTinstanceof _ | JCTmatch _ 
+       | JCTold _ | JCTat _ | JCTcast _ | JCTbitwise_cast _ 
+       | JCTrange_cast _ | JCTreal_cast _ | JCTaddress _ | JCTbase_block _
+-      | JCTrange _ | JCTif _ -> 
++      | JCTlet _ | JCTrange _ | JCTif _ -> 
+ 	  err ()
+     with Failure "linearize" -> 
+       (TermMap.add t (Int 1) TermMap.empty, Int 0)
diff --git a/why-flocq2.patch b/why-flocq2.patch
new file mode 100644
index 0000000..27dda9f
--- /dev/null
+++ b/why-flocq2.patch
@@ -0,0 +1,510 @@
+--- ./lib/coq/WhyFloats.v.orig	2011-10-24 09:21:06.000000000 -0600
++++ ./lib/coq/WhyFloats.v	2012-01-11 15:41:08.873131034 -0700
+@@ -19,17 +19,13 @@ Let emin := (3 - emax - prec)%Z.
+ Let fexp := FLT_exp emin prec.
+ Lemma Hprec': (0 < prec)%Z. revert Hprec. now case Zlt_bool_spec. Qed.
+ Lemma Hemax': (prec < emax)%Z. revert Hemax. now case Zlt_bool_spec. Qed.
+-Let binary_round_correct := binary_round_sign_shl_correct prec emax Hprec' Hemax'.
++Lemma fexp': Valid_exp fexp. apply FLT_exp_valid. apply Hprec'. Qed.
+ 
+ Definition r_to_sd rnd x : binary_float prec emax :=
+   let r := round radix2 fexp (round_mode rnd) x in
+   let m := Ztrunc (scaled_mantissa radix2 fexp r) in
+-  let e := canonic_exponent radix2 fexp r in
+-  match m with
+-  | Z0 => B754_zero prec emax false
+-  | Zpos m => FF2B _ _ _ (proj1 (binary_round_correct rnd false m e))
+-  | Zneg m => FF2B _ _ _ (proj1 (binary_round_correct rnd true m e))
+-  end.
++  let e := canonic_exp radix2 fexp r in
++  binary_normalize prec emax Hprec' Hemax' rnd m e false.
+ 
+ Lemma is_finite_FF2B :
+   forall f H,
+@@ -49,59 +45,19 @@ Theorem r_to_sd_correct :
+   (Rabs r < bpow radix2 emax)%R ->
+   is_finite prec emax (r_to_sd rnd x) = true /\
+   r_to_sd rnd x = r :>R.
+-Proof.
++Proof with auto with typeclass_instances.
+ intros rnd x r Bx.
+ unfold r_to_sd. fold r.
+-assert (Gx: generic_format radix2 fexp r).
+-apply generic_format_round.
+-apply FLT_exp_correct.
+-exact Hprec'.
+-assert (Hr: Z2R (Ztrunc (scaled_mantissa radix2 fexp r)) = scaled_mantissa radix2 fexp r).
+-apply sym_eq.
+-now apply scaled_mantissa_generic.
+-revert Hr.
+-case_eq (Ztrunc (scaled_mantissa radix2 fexp r)).
+-(* *)
+-intros _ Hx.
+-repeat split.
+-apply Rmult_eq_reg_r with (bpow radix2 (- canonic_exponent radix2 fexp r)).
+-now rewrite Rmult_0_l.
+-apply Rgt_not_eq.
+-apply bpow_gt_0.
+-(* *)
+-intros p Hp Hx.
+-case binary_round_correct ; intros Hv.
+-unfold F2R, Fnum, Fexp, cond_Zopp.
+-rewrite Hx, scaled_mantissa_bpow.
+-rewrite round_generic with (1 := Gx).
+-rewrite Rlt_bool_true with (1 := Bx).
+-intros H.
+-split.
+-rewrite is_finite_FF2B.
+-revert H.
+-assert (0 <> r)%R.
+-intros H.
+-rewrite <- H, scaled_mantissa_0 in Hx.
+-now apply (Z2R_neq 0 (Zpos p)).
+-now case binary_round_sign_shl.
+-now rewrite B2R_FF2B.
+-(* *)
+-intros p Hp Hx.
+-case binary_round_correct ; intros Hv.
+-unfold F2R, Fnum, Fexp, cond_Zopp, Zopp.
+-rewrite Hx, scaled_mantissa_bpow.
+-rewrite round_generic with (1 := Gx).
++generalize (binary_normalize_correct prec emax Hprec' Hemax' rnd (Ztrunc (scaled_mantissa radix2 fexp r)) (canonic_exp radix2 fexp r) false).
++unfold r.
++elim generic_format_round...
++fold emin r.
++rewrite round_generic...
+ rewrite Rlt_bool_true with (1 := Bx).
+-intros H.
+-split.
+-rewrite is_finite_FF2B.
+-revert H.
+-assert (0 <> r)%R.
+-intros H.
+-rewrite <- H, scaled_mantissa_0 in Hx.
+-now apply (Z2R_neq 0 (Zneg p)).
+-now case binary_round_sign_shl.
+-now rewrite B2R_FF2B.
++now split.
++apply generic_format_round...
++apply fexp'.
++apply fexp'.
+ Qed.
+ 
+ Theorem r_to_sd_format :
+@@ -109,15 +65,14 @@ Theorem r_to_sd_format :
+   FLT_format radix2 emin prec x ->
+   (Rabs x < bpow radix2 emax)%R ->
+   r_to_sd rnd x = x :>R.
+-Proof.
++Proof with auto with typeclass_instances.
+ intros rnd x Fx Bx.
+ assert (Gx: generic_format radix2 fexp x).
+-apply -> FLT_format_generic.
++apply generic_format_FLT.
+ apply Fx.
+-exact Hprec'.
+-pattern x at 2 ; rewrite <- round_generic with (rnd := round_mode rnd) (1 := Gx).
++pattern x at 2 ; rewrite <- round_generic with (rnd := round_mode rnd) (2 := Gx)...
+ refine (proj2 (r_to_sd_correct _ _ _)).
+-now rewrite round_generic with (1 := Gx).
++rewrite round_generic...
+ Qed.
+ 
+ End r_to_sd.
+@@ -152,10 +107,10 @@ rewrite <- Zsucc_pred.
+ generalize (Zeq_bool_eq _ _ H1). clear.
+ rewrite Fcalc_digits.Z_of_nat_S_digits2_Pnat.
+ intros H.
+-apply (Fcalc_digits.Zpower_gt_digits Fcalc_digits.radix2 (Zpos prec) (Zpos m)).
++apply (Fcalc_digits.Zpower_gt_Zdigits Fcalc_digits.radix2 (Zpos prec) (Zpos m)).
+ revert H.
+ unfold FLT_exp.
+-generalize (Fcalc_digits.digits Fcalc_digits.radix2 (Zpos m)).
++generalize (Fcore_digits.Zdigits Fcalc_digits.radix2 (Zpos m)).
+ intros ; zify ; omega.
+ apply bpow_le.
+ now apply Zle_bool_imp_le.
+@@ -172,6 +127,23 @@ Definition rnd_of_mode (m:mode) :=
+ 
+ (** Single precision *)
+ 
++Definition binary32 := binary_float 24 128.
++
++Let Hprec32 : (0 < 24)%Z.
++apply refl_equal.
++Qed.
++
++Let Hprec32_emax : (24 < 128)%Z.
++apply refl_equal.
++Qed.
++
++Definition b32_opp := Bopp 24 128.
++Definition b32_plus := Bplus _ _ Hprec32 Hprec32_emax.
++Definition b32_minus := Bminus _ _ Hprec32 Hprec32_emax.
++Definition b32_mult := Bmult _ _ Hprec32 Hprec32_emax.
++Definition b32_div := Bdiv _ _ Hprec32 Hprec32_emax.
++Definition b32_sqrt := Bsqrt _ _ Hprec32 Hprec32_emax.
++
+ Record single : Set := mk_single {
+   single_float : binary32;
+   single_value := (single_float : R);
+@@ -229,12 +201,12 @@ Theorem bounded_real_no_overflow_single
+   forall m x,
+   (Rabs x <= max_single)%R ->
+   no_overflow_single m x.
+-Proof.
++Proof with auto with typeclass_instances.
+ intros m x Hx.
+ apply Rabs_le.
+ assert (generic_format radix2 (FLT_exp (-149) 24) max_single).
+-apply generic_format_canonic_exponent.
+-unfold canonic_exponent.
++apply generic_format_F2R.
++unfold canonic_exp.
+ rewrite ln_beta_F2R. 2: easy.
+ rewrite (ln_beta_unique _ _ 24).
+ easy.
+@@ -245,31 +217,40 @@ now apply Z2R_lt.
+ generalize (Rabs_le_inv _ _ Hx).
+ split.
+ erewrite <- round_generic with (x := Ropp max_single).
+-apply round_monotone with (2 := proj1 H0).
+-now apply FLT_exp_correct.
++unfold round_single.
++apply round_le...
++apply FLT_exp_valid. easy.
++easy.
++apply valid_rnd_round_mode.
+ now apply generic_format_opp.
+-rewrite <- round_generic with (rnd := round_mode (rnd_of_mode m)) (1 := H).
+-apply round_monotone with (2 := proj2 H0).
+-now apply FLT_exp_correct.
++unfold round_single.
++apply round_le_generic...
++apply FLT_exp_valid.
++apply Hprec'...
++easy.
+ Qed.
+ 
+ Theorem round_single_monotonic :
+   forall m x y, (x <= y)%R ->
+   (round_single m x <= round_single m y)%R.
+-Proof.
++Proof with auto with typeclass_instances.
+ intros m x y Hxy.
+-apply round_monotone with (2 := Hxy).
+-now apply FLT_exp_correct.
++unfold round_single.
++apply round_le...
++apply FLT_exp_valid.
++apply Hprec'...
+ Qed.
+ 
+ Theorem round_single_idempotent :
+   forall m1 m2 x,
+   round_single m1 (round_single m2 x) = round_single m2 x.
+-Proof.
++Proof with auto with typeclass_instances.
+ intros m1 m2 x.
+ apply round_generic.
+-apply generic_format_round.
+-now apply FLT_exp_correct.
++apply valid_rnd_round_mode.
++apply generic_format_round...
++apply FLT_exp_valid.
++apply Hprec'...
+ Qed.
+ 
+ Theorem round_down_single_neg :
+@@ -295,8 +276,9 @@ Theorem round_single_down_le :
+   (round_single down x <= x)%R.
+ Proof.
+ intros x.
+-eapply round_DN_pt.
+-now apply FLT_exp_correct.
++eapply round_DN_pt...
++apply FLT_exp_valid.
++apply Hprec'. easy.
+ Qed.
+ 
+ Theorem round_up_single_ge :
+@@ -305,12 +287,30 @@ Theorem round_up_single_ge :
+ Proof.
+ intros x.
+ apply Rle_ge.
+-eapply round_UP_pt.
+-now apply FLT_exp_correct.
++eapply round_UP_pt...
++apply FLT_exp_valid.
++apply Hprec'. easy.
+ Qed.
+ 
+ (** Double precision *)
+ 
++Definition binary64 := binary_float 53 1024.
++
++Let Hprec64 : (0 < 53)%Z.
++apply refl_equal.
++Qed.
++
++Let Hprec64_emax : (53 < 1024)%Z.
++apply refl_equal.
++Qed.
++
++Definition b64_opp := Bopp 53 1024.
++Definition b64_plus := Bplus _ _ Hprec64 Hprec64_emax.
++Definition b64_minus := Bminus _ _ Hprec64 Hprec64_emax.
++Definition b64_mult := Bmult _ _ Hprec64 Hprec64_emax.
++Definition b64_div := Bdiv _ _ Hprec64 Hprec64_emax.
++Definition b64_sqrt := Bsqrt _ _ Hprec64 Hprec64_emax.
++
+ Record double : Set := mk_double {
+   double_float : binary64;
+   double_value := (double_float : R);
+@@ -368,12 +368,12 @@ Theorem bounded_real_no_overflow_double
+   forall m x,
+   (Rabs x <= max_double)%R ->
+   no_overflow_double m x.
+-Proof.
++Proof with auto with typeclass_instances.
+ intros m x Hx.
+ apply Rabs_le.
+ assert (generic_format radix2 (FLT_exp (-1074) 53) max_double).
+-apply generic_format_canonic_exponent.
+-unfold canonic_exponent.
++apply generic_format_F2R.
++unfold canonic_exp.
+ rewrite ln_beta_F2R. 2: easy.
+ rewrite (ln_beta_unique _ _ 53).
+ easy.
+@@ -384,31 +384,40 @@ now apply Z2R_lt.
+ generalize (Rabs_le_inv _ _ Hx).
+ split.
+ erewrite <- round_generic with (x := Ropp max_double).
+-apply round_monotone with (2 := proj1 H0).
+-now apply FLT_exp_correct.
++unfold round_double.
++apply round_le...
++apply FLT_exp_valid. easy.
++easy.
++apply valid_rnd_round_mode.
+ now apply generic_format_opp.
+-rewrite <- round_generic with (rnd := round_mode (rnd_of_mode m)) (1 := H).
+-apply round_monotone with (2 := proj2 H0).
+-now apply FLT_exp_correct.
++unfold round_double.
++apply round_le_generic...
++apply FLT_exp_valid.
++apply Hprec'...
++easy.
+ Qed.
+ 
+ Theorem round_double_monotonic :
+   forall m x y, (x <= y)%R ->
+   (round_double m x <= round_double m y)%R.
+-Proof.
++Proof with auto with typeclass_instances.
+ intros m x y Hxy.
+-apply round_monotone with (2 := Hxy).
+-now apply FLT_exp_correct.
++unfold round_double.
++apply round_le...
++apply FLT_exp_valid.
++apply Hprec'...
+ Qed.
+ 
+ Theorem round_double_idempotent :
+   forall m1 m2 x,
+   round_double m1 (round_double m2 x) = round_double m2 x.
+-Proof.
++Proof with auto with typeclass_instances.
+ intros m1 m2 x.
+ apply round_generic.
+-apply generic_format_round.
+-now apply FLT_exp_correct.
++apply valid_rnd_round_mode.
++apply generic_format_round...
++apply FLT_exp_valid.
++apply Hprec'...
+ Qed.
+ 
+ Theorem round_down_double_neg :
+@@ -434,8 +443,9 @@ Theorem round_double_down_le :
+   (round_double down x <= x)%R.
+ Proof.
+ intros x.
+-eapply round_DN_pt.
+-now apply FLT_exp_correct.
++eapply round_DN_pt...
++apply FLT_exp_valid.
++apply Hprec'. easy.
+ Qed.
+ 
+ Theorem round_up_double_ge :
+@@ -444,8 +454,9 @@ Theorem round_up_double_ge :
+ Proof.
+ intros x.
+ apply Rle_ge.
+-eapply round_UP_pt.
+-now apply FLT_exp_correct.
++eapply round_UP_pt...
++apply FLT_exp_valid.
++apply Hprec'. easy.
+ Qed.
+ 
+ (** Quad precision *)
+@@ -566,8 +577,8 @@ unfold F2R. simpl.
+ split.
+ now rewrite Rmult_1_r.
+ now split.
+-apply <- FLT_format_generic.
+-2: easy.
++apply FLT_format_generic.
++apply Hprec'. easy.
+ change 2%Z with (radix_val radix2) in Bz.
+ destruct z as [|z|z] ; unfold Zabs in Bz.
+ apply generic_format_0.
+--- ./lib/coq/WhyFloatsStrict.v.orig	2011-10-24 09:21:06.000000000 -0600
++++ ./lib/coq/WhyFloatsStrict.v	2012-01-11 15:42:11.453663887 -0700
+@@ -155,30 +155,13 @@ repeat split.
+ exact H2.
+ Qed.
+ 
+-Axiom Bplus_correct : (* the statement from Flocq 1.4 is not strong enough;
+-                         the axiom can be removed once the library is converted to Flocq 2.0 *)
+-  forall (prec emax : Z) (Hprec : (0 < prec)%Z) (Hmax : (prec < emax)%Z)
+-         (m : Fappli_IEEE.mode) (x y : binary_float prec emax),
+-  is_finite prec emax x = true ->
+-  is_finite prec emax y = true ->
+-  if Rlt_bool (Rabs (round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode m)
+-       (B2R prec emax x + B2R prec emax y))) (bpow radix2 emax)
+-  then
+-    B2R prec emax (Bplus prec emax Hprec Hmax m x y) =
+-      round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode m) (B2R prec emax x + B2R prec emax y) /\
+-    is_finite prec emax (Bplus prec emax Hprec Hmax m x y) = true
+-  else
+-    B2FF prec emax (Bplus prec emax Hprec Hmax m x y) =
+-      binary_overflow prec emax m (Bsign prec emax x) /\
+-    Bsign prec emax x = Bsign prec emax y.
+-
+ Lemma add_single_specification :
+   forall m (x y : single),
+   no_overflow_single m (single_value x + single_value y) ->
+   exists z, add_single_post m x y z.
+ Proof.
+ intros m x y Br.
+-refine (_ (Bplus_correct 24 128 (refl_equal Lt) (refl_equal Lt) (rnd_of_mode m) (single_float x) (single_float y)
++refine (_ (Bplus_correct 24 128 Hprec32 Hprec32_emax (rnd_of_mode m) (single_float x) (single_float y)
+   (single_finite x) (single_finite y))).
+ rewrite Rlt_bool_true.
+ 2: now apply no_overflow_single_bounded.
+@@ -189,27 +172,13 @@ repeat split.
+ exact H1.
+ Qed.
+ 
+-Axiom Bmult_correct : (* the statement from Flocq 1.4 is not strong enough;
+-                         the axiom can be removed once the library is converted to Flocq 2.0 *)
+-  forall (prec emax : Z) (Hprec : (0 < prec)%Z) (Hmax : (prec < emax)%Z)
+-         (m : Fappli_IEEE.mode) (x y : binary_float prec emax),
+-  if Rlt_bool (Rabs (round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode m)
+-       (B2R prec emax x * B2R prec emax y))) (bpow radix2 emax)
+-  then
+-    B2R prec emax (Bmult prec emax Hprec Hmax m x y) =
+-      round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode m) (B2R prec emax x * B2R prec emax y) /\
+-    is_finite prec emax (Bmult prec emax Hprec Hmax m x y) = andb (is_finite prec emax x) (is_finite prec emax y)
+-  else
+-    B2FF prec emax (Bmult prec emax Hprec Hmax m x y) =
+-      binary_overflow prec emax m (xorb (Bsign prec emax x) (Bsign prec emax y)).
+-
+ Lemma mul_single_specification :
+   forall m (x y : single),
+   no_overflow_single m (single_value x * single_value y) ->
+   exists z, mul_single_post m x y z.
+ Proof.
+ intros m x y Br.
+-refine (_ (Bmult_correct 24 128 (refl_equal Lt) (refl_equal Lt) (rnd_of_mode m) (single_float x) (single_float y))).
++refine (_ (Bmult_correct 24 128 Hprec32 Hprec32_emax (rnd_of_mode m) (single_float x) (single_float y))).
+ rewrite Rlt_bool_true.
+ 2: now apply no_overflow_single_bounded.
+ fold b32_mult.
+@@ -220,28 +189,13 @@ repeat split.
+ exact H1.
+ Qed.
+ 
+-Axiom Bdiv_correct : (* the statement from Flocq 1.4 is not strong enough;
+-                        the axiom can be removed once the library is converted to Flocq 2.0 *)
+-  forall (prec emax : Z) (Hprec : (0 < prec)%Z) (Hmax : (prec < emax)%Z)
+-    (m : Fappli_IEEE.mode) (x y : binary_float prec emax),
+-  B2R prec emax y <> 0%R ->
+-  if Rlt_bool (Rabs (round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode m)
+-       (B2R prec emax x / B2R prec emax y))) (bpow radix2 emax)
+-  then
+-    B2R prec emax (Bdiv prec emax Hprec Hmax m x y) =
+-      round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode m) (B2R prec emax x / B2R prec emax y) /\
+-    is_finite prec emax (Bdiv prec emax Hprec Hmax m x y) = is_finite prec emax x
+-  else
+-    B2FF prec emax (Bdiv prec emax Hprec Hmax m x y) =
+-      binary_overflow prec emax m (xorb (Bsign prec emax x) (Bsign prec emax y)).
+-
+ Lemma div_single_specification :
+   forall m (x y : single), single_value y <> R0 ->
+   no_overflow_single m (single_value x / single_value y) ->
+   exists z, div_single_post m x y z.
+ Proof.
+ intros m x y Zy Br.
+-refine (_ (Bdiv_correct 24 128 (refl_equal Lt) (refl_equal Lt) (rnd_of_mode m) (single_float x) (single_float y) Zy)).
++refine (_ (Bdiv_correct 24 128 Hprec32 Hprec32_emax (rnd_of_mode m) (single_float x) (single_float y) Zy)).
+ rewrite Rlt_bool_true.
+ 2: now apply no_overflow_single_bounded.
+ fold b32_div.
+@@ -252,20 +206,12 @@ repeat split.
+ exact H1.
+ Qed.
+ 
+-Axiom Bsqrt_correct : (* the statement from Flocq 1.4 is not strong enough;
+-                         the axiom can be removed once the library is converted to Flocq 2.0 *)
+-  forall (prec emax : Z) (Hprec : (0 < prec)%Z) (Hmax : (prec < emax)%Z)
+-         (m : Fappli_IEEE.mode) (x : binary_float prec emax),
+-  B2R prec emax (Bsqrt prec emax Hprec Hmax m x) =
+-    round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode m) (sqrt (B2R prec emax x)) /\
+-  is_finite prec emax (Bsqrt prec emax Hprec Hmax m x) = match x with B754_zero _ => true | B754_finite false _ _ _ => true | _ => false end.
+-
+ Lemma sqrt_single_specification :
+   forall m (x : single), Rle 0 (single_value x) ->
+   exists z, sqrt_single_post m x z.
+ Proof.
+ intros m x Zx.
+-refine (_ (Bsqrt_correct 24 128 (refl_equal Lt) (refl_equal Lt) (rnd_of_mode m) (single_float x))).
++refine (_ (Bsqrt_correct 24 128 Hprec32 Hprec32_emax (rnd_of_mode m) (single_float x))).
+ fold b32_sqrt.
+ intros (H1, H2).
+ assert (is_finite 24 128 (b32_sqrt (rnd_of_mode m) (single_float x)) = true).
+--- ./lib/coq/JessieGappa.v.orig	2011-10-24 09:21:06.000000000 -0600
++++ ./lib/coq/JessieGappa.v	2012-01-11 15:41:08.874131235 -0700
+@@ -571,7 +571,7 @@ unfold min_gen_float, min_float2.
+ case F ; apply bpow_gt_0.
+ rewrite <- round_of_min_gen with F m.
+ revert Bx1.
+-case F ; apply round_monotone ; now apply FLT_exp_correct.
++case F ; apply round_le...
+ Save.
+ 
+ Lemma negative_constant : forall f m x, 
+@@ -592,7 +592,7 @@ case F ; apply bpow_ge_0.
+ apply Rle_lt_trans with (- min_gen_float F)%R.
+ rewrite <- round_of_opp_min_gen with F m.
+ revert Bx2.
+-case F ; apply round_monotone ; now apply FLT_exp_correct.
++case F ; apply round_le...
+ apply Ropp_lt_gt_0_contravar.
+ unfold min_gen_float, min_float2.
+ case F ; apply bpow_gt_0.
+@@ -602,7 +602,7 @@ Lemma round_increasing: forall f m x y,
+       (x <= y)%R -> (round_float f m x <= round_float f m y)%R.
+ Proof.
+ intros F m x y.
+-case F ; apply round_monotone ; now apply FLT_exp_correct.
++case F ; apply round_le...
+ Save.
+ 
+ Lemma round_greater_min: forall f m x, 
diff --git a/why.spec b/why.spec
new file mode 100644
index 0000000..1ff7d47
--- /dev/null
+++ b/why.spec
@@ -0,0 +1,556 @@
+# Whether coq is available
+%ifarch %{ocaml_arches}
+%global has_coq 1
+%else
+%global has_coq 0
+%endif
+
+# Whether PVS is available
+%ifarch %{ix86} x86_64 ppc sparcv9
+%global has_pvs 1
+%else
+%global has_pvs 0
+%endif
+
+# What kind of ocaml build to do
+%global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)
+
+# Don't create debuginfo; it's not particularly useful for OCaml programs.
+%global debug_package %{nil}
+
+Name:           why
+Version:        2.30
+Release:        5%{?dist}
+Summary:        Software verification platform
+
+Group:          Applications/Engineering
+License:        LPGLv2 with exceptions
+URL:            http://why.lri.fr/
+Source0:        http://why.lri.fr/download/why-%{version}.tar.gz
+Source1:        README.why-gwhy.Fedora
+Source2:        README.why-coq.Fedora
+Source3:        README.why
+Source4:        gwhy.desktop
+Source5:        gwhy-icon.png
+Source6:        min.mlw
+Source7:        min_why.why.result
+Source8:        http://krakatoa.lri.fr/manual/krakatoa.pdf
+Source9:        jessie.desktop
+Source10:       div.pvs
+Source11:       rem.pvs
+Source12:       patch_jessie_pvs
+
+# The gwhy execution shell script is not particularly informative
+# about when bad parameters are passed to it - this patch fixes that.
+# Upstream has been informed about this issue and a better fix is on
+# their todo list
+Patch0:         gwhy-2.26.patch
+
+# This patch makes a Fedora-specific fix to eliminate checking for the
+# location of Coq - since we're using the coq package, we know where
+# it is and their checking causes the rpm building to fail.
+# It also makes a fix necessary to correctly build the bytecode only
+# version of why by building the make_float_model tool correctly in
+# this case.
+Patch1:         why-2.30-Makefile.in.patch
+
+# This patch fixes some mildly bitrotted APRON support code.
+# Applied upstream.
+Patch2:         why-apron.patch
+
+# This patch updates the flocq usage for flocq 2.0.0.  It will be sent upstream.
+Patch3:         why-flocq2.patch
+
+BuildRequires:  auto-destdir
+BuildRequires:  cvc3
+BuildRequires:  desktop-file-utils
+BuildRequires:  emacs-nox xemacs xemacs-packages-extra
+BuildRequires:  frama-c-devel
+BuildRequires:  gappalib-coq
+BuildRequires:  gtk2-devel
+BuildRequires:  ocaml
+BuildRequires:  ocaml-apron-devel
+BuildRequires:  ocaml-camlp4-devel
+BuildRequires:  ocaml-lablgtk-devel
+BuildRequires:  ocaml-ocamldoc
+BuildRequires:  ocaml-ocamlgraph-devel
+%if %{has_coq}
+BuildRequires:  coq
+%endif
+%if %{has_pvs}
+BuildRequires:  pvs
+%endif
+
+# Only build on arches that support ocaml
+ExclusiveArch: %{ocaml_arches}
+
+# Filter out names that should not be exposed externally
+%global __requires_exclude ocaml\\\(((Ast)|(Cc)|(Env)|(Error)|(Loc)|(Logic)|(Logic_decl)|(Misc)|(Parser)|(Project)|(Ptree)|(Types))\\\)
+%global __provides_exclude ocaml\\\(((Lexer)|(Lib)|(Loc)|(Output)|(Parser)|(Project)|(Report)|(Xml))\\\)
+
+%description
+Why is a software verification platform that applies formal proving
+tools to annotated programs.  It is currently capable of analysis of C
+(through "Frama-C"), Java (through the included tool "Krakatoa"), and
+potentially ML programs with some modification into Why's own ML-like
+language.  Furthermore, Why is capable of analysis of any program that
+is mapped onto its own internal language.  It uses a weakest
+precondition involving calculus to generate potential theorems necessary
+for the proof of a program's correctness.  It translates these theorems
+into formats that can be used by external proof assistants (without any
+extra work Coq, PVS, HOL Light, and Mizar are supported - having one is
+recommended and both Coq and PVS are packaged for Fedora) and automated
+theorem provers (without any extra work Simplify, Alt-Ergo, Yices, Z3,
+CVC3, and Zenon are supported and Alt-Ergo, CVC3, and Zenon are packaged
+for Fedora) so that these results can be externally proven, resulting in
+a proof of program correctness.
+
+Note: Each user account must be set up by running "why-config" at the
+command line (to set up a configuration file).
+
+%package gwhy
+Group:          Applications/Engineering
+Summary:        IDE for Why software verification platform
+Requires:       %{name}%{?_isa} = %{version}-%{release}, zenity
+
+%description gwhy
+Gwhy is an optional graphical user interface for the Why software
+coordination platform.  It assists in the coordination of dispatching
+assertions that need to be proven to different theorem provers by
+providing an interface to do this and also supports inspection of why
+input files.
+
+%package jessie
+Group:          Applications/Engineering
+Summary:        Interface between why and frama-c
+Requires:       %{name}%{?_isa} = %{version}-%{release}
+Requires:       frama-c
+
+%description jessie
+The Jessie plugin, an interface between why and frama-c.  Invoke it with:
+  frama-c -jessie FILE.c
+
+%if %{has_coq}
+%package coq
+Group:          Applications/Engineering
+Summary:        Libraries for interfacing Coq with Why
+Requires:       %{name}%{?_isa} = %{version}-%{release}
+Requires:       gappalib-coq
+
+%description coq
+This package contains a set of routines that assist in the manipulation
+of why Coq-formatted output within Coq.
+%endif
+
+%if %{has_pvs}
+# Why's integration with PVS depends on the NASA Langley PVS Libraries,
+# which have no license information.  This provides an alternative:
+%package pvs-support
+Group:          Applications/Engineering
+Summary:        Complete Why software verification platform suite
+Requires:       %{name}%{?_isa} = %{version}-%{release}
+Requires:       pvs
+
+%description pvs-support
+This package provides support definitions so that the Why software
+verification platform suite can invoke PVS without licensing issues.
+%endif
+
+%package emacs
+Summary:        Emacs support file for why files
+Group:          Development/Languages
+Requires:       %{name} = %{version}-%{release}
+Requires:       emacs(bin)
+BuildArch:      noarch
+
+%description emacs
+This package contains an Emacs support file for working with why files.
+
+%package emacs-el
+Summary:        Emacs source file for why support
+Group:          Development/Languages
+Requires:       %{name}-emacs = %{version}-%{release}
+BuildArch:      noarch
+
+%description emacs-el
+This package contains the Emacs source file for the Emacs why support.
+This package is not needed to use the Emacs support.
+
+%package xemacs
+Summary:        XEmacs support file for why files
+Group:          Development/Languages
+Requires:       %{name} = %{version}-%{release}
+Requires:       xemacs(bin)
+BuildArch:      noarch
+
+%description xemacs
+This package contains an XEmacs support file for working with why files.
+
+%package xemacs-el
+Summary:        XEmacs source file for why support
+Group:          Development/Languages
+Requires:       %{name}-xemacs = %{version}-%{release}
+BuildArch:      noarch
+
+%description xemacs-el
+This package contains the XEmacs source file for the XEmacs why support.
+This package is not needed to use the Emacs support.
+
+%package all
+Group:          Applications/Engineering
+Summary:        Complete Why software verification platform suite
+Requires:       why%{?_isa} = %{version}-%{release}
+Requires:       why-gwhy%{?_isa} = %{version}-%{release}
+Requires:       why-jessie%{?_isa} = %{version}-%{release}
+%if %{has_coq}
+Requires:       why-coq%{?_isa} = %{version}-%{release}
+%endif
+%if %{has_pvs}
+Requires:       why-pvs-support%{?_isa} = %{version}-%{release}
+%endif
+Requires:       alt-ergo cvc3 gappalib-coq zenon
+
+%description all
+This package provides a complete software verification platform suite
+based on Why, including various automated and interactive provers.
+
+%prep
+%setup -q
+%patch0
+%patch1
+%patch2
+%patch3
+
+cp -p %SOURCE1 %SOURCE2 %SOURCE6 %SOURCE7 ./
+
+# Fix missing DESTDIRs in the makefile
+sed -e 's|$(COQLIB)/user-contrib/Why|$(DESTDIR)$(COQLIB)/user-contrib/Why|' \
+    -e 's|$(PVSLIB)/why|$(DESTDIR)$(PVSLIB)/why|' \
+    -i Makefile.in
+
+%define fix_encoding() \
+  iconv -f %2 -t %3 %1 > %1.utf8; \
+  touch -r %1 %1.utf8; \
+  mv -f %1.utf8 %1;
+
+# Fix encodings
+for f in CHANGES COPYING examples/bresenham/bresenham.mlw \
+  examples/bresenham/bresenham_coq.mlw examples/bresenham/bresenham_inv.mlw \
+  examples/edit-distance/distance.mlw examples/heapsort/downheap.mlw \
+  examples/heapsort/heapsort.mlw examples/heapsort/Inftree.v \
+  examples/kmp/kmp.mlw examples/kmp/Lex.v examples/kmp/Match.v \
+  examples/kmp/Next.v examples/misc/matrix.why examples/misc/matrix_why.v \
+  examples/quicksort/partition.mlw examples/quicksort/Partition.v \
+  examples/quicksort/quicksort.mlw examples/quicksort/Quicksort.v \
+  examples/sqrt/sqrt.mlw examples/string-matching/Match.v; do
+  %fix_encoding $f ISO-8859-1 UTF-8
+done
+
+# Fix a doubly utf8-encoded file
+%fix_encoding examples/sqrt/sqrt_why.v UTF-8 ISO-8859-1
+
+# Fix line endings
+for f in examples-c/tutorial/average.c examples-c/tutorial/purse.c \
+  examples-c/ukkonen/main.c examples-c/ukkonen/ukkonen.c; do
+  sed "s/\r//" $f > $f.new
+  touch -r $f $f.new
+  mv -f $f.new $f
+done
+
+# APRON support: add a missing include and a missing rpath
+sed -e "s|-I +apron|-I +apron -I +mlgmpidl|" \
+    -e "s|-lpolkaMPQ_caml|-Wl,-rpath,%{_libdir}/ocaml/apron|" \
+    -i configure
+
+%build
+%if ! %{opt}
+%global opt_option OCAMLBEST=byte OCAMLC=ocamlc OCAMLDEP=ocamldep OCAMLYACC=ocamlyacc OCAMLLEX=ocamllex
+%else
+%global opt_option OCAMLBEST=opt OCAMLOPT=ocamlopt.opt
+%endif
+
+# Update the version numbers of external programs
+# Also, command "pvs" is LVM2's /sbin/pvs, so rename "pvs" to pvs-sbcl:
+sed -e 's/versions_ok = \["0\.93"\]/versions_ok = ["0.93";"0.94"]/' \
+    -e 's/versions_ok = \["1\.0\.25";.*\]/versions_ok = ["1.0.31"]/' \
+    -e 's/versions_ok = \["2.2"\]/versions_ok = ["2.4.1"]/' \
+    -e 's/versions_ok = \["8\.0";.*\]/versions_ok = ["8.3pl2"]/' \
+    -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"]);/' \
+    -i tools/dpConfig.ml
+sed -e 's/pvs/pvs-sbcl/' -i configure
+
+%if %{has_coq}
+%configure --enable-apron --enable-verbosemake
+%else
+%configure --enable-apron --enable-verbosemake COQC=no
+%endif
+make %{opt_option}
+
+# Strip binaries (the Makefile misses some of them)
+strip bin/why-cpulimit
+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
+%endif
+
+%install
+# Avoid a bug in PVS batch mode when using emacs
+make install DESTDIR=%{buildroot} %{opt_option} PVSLIB=%{_libdir}/pvs/lib \
+     PVSEMACS=xemacs
+
+# Fix a small bug in their Makefile: if no Coq, NO .v files should be installed
+%if ! %{has_coq}
+rm -f `find %{buildroot}%{_datadir}/coq -name '*.v'`
+%endif
+
+# If no PVS, no .pvs files should be installed
+%if ! %{has_pvs}
+rm -fr %{buildroot}%{_libdir}/pvs
+%endif
+
+# Install desktop icon and menu entry
+%global why_data_dir %{_datadir}/why
+mkdir -p %{buildroot}%{why_data_dir}
+cp -p %{SOURCE5} %{buildroot}%{why_data_dir}
+sed -e 's|ICON-LOCATION-BASE|%{why_data_dir}|' %{SOURCE4} > gwhy.desktop
+desktop-file-install --vendor="fedora" \
+ --dir=%{buildroot}%{_datadir}/applications gwhy.desktop
+sed -e 's|ICON-LOCATION-BASE|%{why_data_dir}|' %{SOURCE9} > jessie.desktop
+desktop-file-install --vendor="fedora" \
+ --dir=%{buildroot}%{_datadir}/applications jessie.desktop
+
+%if %{has_pvs}
+# Get rid of a BUILDROOT reference in a log file (fails QA_CHECK_RPATHS)
+sed -i "s|%{buildroot}||" %{buildroot}%{_libdir}/pvs/lib/why/top.out
+
+mkdir -p                      %{buildroot}%{_libdir}/pvs/lib/ints/
+cp -p %{SOURCE10} %{SOURCE11} %{buildroot}%{_libdir}/pvs/lib/ints/
+cp -p %{SOURCE12}             %{buildroot}%{_bindir}/
+%endif
+
+%global why_doc_dir %{_defaultdocdir}/%{name}-%{version}
+%global why_examples_dir %{why_doc_dir}/examples/
+
+# Fix up documentation and examples
+mkdir -p %{buildroot}%{why_examples_dir}mlw/
+mkdir -p %{buildroot}%{why_examples_dir}c/
+cp -p doc/manual.ps %{buildroot}%{why_doc_dir}/why-manual.ps
+cp -p %{SOURCE8} %{SOURCE3} CHANGES COPYING LICENSE README Version %{buildroot}%{why_doc_dir}
+
+# Copy in the example files, leaving behind all generated files
+cd examples
+for d in `find -mindepth 1 -maxdepth 1 -type d`; do
+ mkdir -p %{buildroot}%{why_examples_dir}mlw/$d
+done
+for f in `find -regex '.*\(\.mlw\|\.why\)' | grep -E -v '_inv|_coq|_why'`; do
+ cp -p $f %{buildroot}%{why_examples_dir}mlw/$f
+done
+
+cd ../examples-c
+for d in `find -mindepth 1 -maxdepth 1 -type d`; do
+ mkdir -p %{buildroot}%{why_examples_dir}c/$d
+done
+for f in `find -regex '.*\.c'`; do
+ cp -p $f %{buildroot}%{why_examples_dir}c/$f
+done
+
+# Remove a stray coq file (already installed in the right place)
+rm -f %{buildroot}%{_libdir}/coq/jessie_why.v
+
+# Move the Emacs support file to the right places and byte compile it
+cd ..
+mkdir -p %{buildroot}%{_emacs_sitelispdir}
+cp -p lib/emacs/why.el %{buildroot}%{_emacs_sitelispdir}
+mkdir -p %{buildroot}%{_xemacs_sitelispdir}
+cp -p lib/emacs/why.el %{buildroot}%{_xemacs_sitelispdir}
+cd %{buildroot}%{_emacs_sitelispdir}
+%{_emacs_bytecompile} why.el
+cd %{buildroot}%{_xemacs_sitelispdir}
+%{_xemacs_bytecompile} why.el
+rm -fr %{buildroot}%{_libdir}/why/emacs
+
+%check
+%if %opt
+%global why bin/why.opt
+%else
+%global why bin/why.byte
+%endif
+WHYLIB=lib %why --why --output min.why min.mlw
+diff -u min.why min_why.why.result  # Show differences from correct result.
+
+%files
+%{_bindir}/*
+%{_libdir}/why/
+%{_mandir}/man1/why.1*
+%{why_doc_dir}/
+# This last example is really an example only for Coq - only .v files
+%exclude %{why_examples_dir}mlw/string-matching/
+# why-gwhy:
+%exclude %{_bindir}/gwhy*
+# why-jessie
+%exclude %{_bindir}/jessie
+# why-pvs-support:
+%exclude %{_bindir}/patch_jessie_pvs
+
+%files gwhy
+%doc README.why-gwhy.Fedora
+%{_bindir}/gwhy
+%{_bindir}/gwhy-bin
+%{why_data_dir}/
+%{_datadir}/applications/fedora-gwhy.desktop
+
+%files jessie
+%{_bindir}/jessie
+%{_libdir}/jessie/
+%{_libdir}/frama-c/plugins/Jessie.*
+%{_datadir}/applications/fedora-jessie.desktop
+
+%if %{has_coq}
+%files coq
+%doc README.why-coq.Fedora
+%{_libdir}/coq/user-contrib/Why/
+%endif
+
+%if %{has_pvs}
+%files pvs-support
+%{_libdir}/pvs/lib/*
+%{_bindir}/patch_jessie_pvs
+%endif
+
+%files emacs
+%{_emacs_sitelispdir}/why.elc
+
+%files emacs-el
+%{_emacs_sitelispdir}/why.el
+
+%files xemacs
+%{_xemacs_sitelispdir}/why.elc
+
+%files xemacs-el
+%{_xemacs_sitelispdir}/why.el
+
+# "why-all" is a meta-package; it just depends on other packages, so that
+# it's easier to install a useful suite of tools.  Thus, it has no files:
+%files all
+
+
+%changelog
+* Wed Jan 11 2012 Jerry James <loganjerry@gmail.com> - 2.30-5
+- Patch to work with flocq 2.0.0
+
+* Tue Dec 27 2011 Jerry James <loganjerry@gmail.com> - 2.30-4
+- Rebuild for coq 8.3pl3
+
+* Tue Dec  6 2011 Jerry James <loganjerry@gmail.com> - 2.30-3
+- Update alt_ergo and yices "okay" version numbers
+
+* Wed Nov 23 2011 Jerry James <loganjerry@gmail.com> - 2.30-2
+- Rebuild with APRON and gappalib-coq support
+
+* Fri Oct 28 2011 Jerry James <loganjerry@gmail.com> - 2.30-1
+- New upstream release
+
+* Thu Jul 14 2011 Jerry James <loganjerry@gmail.com> - 2.29-2
+- Fix broken conditionals
+
+* Mon Jul 11 2011 Jerry James <loganjerry@gmail.com> - 2.29-1
+- New upstream release (fixes FTBFS: bz 715902)
+- Remove unnecessary spec file elements (BuildRoot, etc.)
+- Update approach to filtering provides and requires
+- Add has_pvs analogously to has_coq, and simplify macro usage
+- Add (X)Emacs support packages
+- New subpackage for the jessie plugin to avoid unowned directories and
+  permit a direct dependency on frama-c
+- Prepare for the eventual availability of APRON
+
+* Thu Apr 14 2011 Karsten Hopp <karsten@redhat.com> 2.28-2.2
+- add ppc to excludearch, too. No pvs-sbcl available there
+
+* Wed Apr 13 2011 Karsten Hopp <karsten@redhat.com> 2.28-2.1
+- add ppc64 to excludearch, no sbcl available there
+
+* Mon Feb 07 2011 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.28-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_15_Mass_Rebuild
+
+* Fri Jan 21 2011 Richard W.M. Jones <rjones@gmail.com> - 2.28-1
+- Since 2.26 FTBFS, try latest upstream (2.28).
+- Rebase Makefile.in patch.
+- Fix(?) test result.
+- No libdir/frama-c directory is created any more.
+
+* Fri Jan 21 2011 Richard W.M. Jones <rjones@gmail.com> - 2.26-2
+- Bump and rebuild for OCaml 3.12.
+
+* Sat Oct 09 2010 David A. Wheeler + Mark Rader <dwheeler@dwheeler.com> - 2.26-1
+- Upgrade to upstream version 2.26 (inc. update of krakatoa.pdf)
+- Integrated with Frama-C and PVS (as pvs-sbcl)
+
+* Mon Jan 11 2010 Richard W.M. Jones <rjones@gmail.com> - 2.23-2
+- Rebuild to fix dependencies.
+
+* Fri Jan 08 2010 Alan Dunn <amdunn@gmail.com> - 2.23-1
+- Upgrade to upstream version 2.23
+- Move execstack fixing to spec file from patch
+- Moved patch descriptions to initial patch declaration as in examples
+  in Fedora documentation
+- New Caduceus, Krakatoa documentation
+- Update test result from small test min.mlw
+- Added CVC3 interfacing capabilities
+- Removed patch for gwhy configuration, as there is a new mechanism for this
+
+* Tue Sep 22 2009 Dennis Gilmore <dennis@ausil.us> - 2.17-5
+- Exclude sparc64 s390 s390x  there is no ocaml there
+
+* Fri Aug 07 2009 Alan Dunn <amdunn@gmail.com> - 2.17-4
+- Removed now irrelevant check for no OCaml in Fedora < 9 (those
+  distributions are EOL)
+- Changed ExcludeArch to proper Fedora versions
+- Builds coq subpackage exactly when Coq can be built, thus making
+  build independent of whether Coq can be built
+- define -> global
+- Fixed accidental use of in tar ocamlgraph instead of one that is
+  separately packaged
+
+* Mon Jul 27 2009 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.17-3
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_12_Mass_Rebuild
+
+* Wed Feb 25 2009 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.17-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_11_Mass_Rebuild
+
+* Wed Dec 24 2008 Alan Dunn <amdunn@gmail.com> 2.17-1
+- Upgrade to version 2.17 (bz: 477790)
+- Add ownership of two directories common with Coq, but neither program requires the other (bz: 474016)
+- Minor filename change in 2.17 (GPL -> LICENSE)
+- Added back Coq .v files to match policy for Coq
+- Changed directory structure re: jessie and krakatoa to match new structure in 2.17
+- Minor changes to patches to ensure they still work in 2.17
+- Corrected package location gwhy-icon.png (should only be in gwhy)
+* Tue Aug 5 2008 Alan Dunn <amdunn@gmail.com> 2.14-2.1
+- ExcludeArch ppc64 on Fedora 8 due to no ocaml.
+* Fri Aug 1 2008 Alan Dunn <amdunn@gmail.com> 2.14-2
+- Fixed minor issues in response to package review:
+- Inclusion of COPYING, GPL license-related files
+- Added config.mll patch to make default config file created nicer
+- Changes subpackage dependencies to be fully versioned.
+- Makes during build allowed to be noisy (allowed to print).
+* Wed Jul 30 2008 Alan Dunn <amdunn@gmail.com> 2.14-1
+- Changed to new version of why, removed previous why-cpulimit name
+  change, zenon output format patches as the issues were fixed in
+  why 2.14.
+- Moved doc subpackage back into main package.
+- Added example files to documentation subpackage.
+- Added check section with test on small why file.
+- Reformatted some macro names for greater readability.
+* Thu Jul 24 2008 Alan Dunn <amdunn@gmail.com> 2.13-2
+- Added several patches: fixed Zenon output, completed fix of rename
+  of cpulimit -> why-cpulimit.
+* Wed Jul 23 2008 Alan Dunn <amdunn@gmail.com> 2.13-1
+- Initial Fedora RPM version.
+
+# TODO:
+# If file $HOME/.gwhyrc does not exist, autorun "why-config".
+# Finish packaging/integrating "APRON" (for Inference of annotations)
+