[gappalib-coq] More changes necessary to work with coq 8.4.

[Jerry James]

commit 7de42348abcc4ca373c12f5a784d69e636ff5097
Author: Jerry James <jamesjer at betterlinux.com>
Date:   Wed Aug 22 17:02:12 2012 -0600

    More changes necessary to work with coq 8.4.

 gappalib-coq-coq84.patch |   71 ++++++++++++++++++++++++++++++++++++++++++++++
 gappalib-coq.spec        |    6 ++--
 2 files changed, 74 insertions(+), 3 deletions(-)
---
diff --git a/gappalib-coq-coq84.patch b/gappalib-coq-coq84.patch
new file mode 100644
index 0000000..8a6d074
--- /dev/null
+++ b/gappalib-coq-coq84.patch
@@ -0,0 +1,71 @@
+--- ./src/gappatac.ml.orig	2011-12-24 09:02:53.000000000 -0700
++++ ./src/gappatac.ml	2012-08-22 16:57:48.106641575 -0600
+@@ -655,7 +655,7 @@ let no_glob f =
+ 
+ (** replace all evars of any type [ty] by [(refl_equal true : ty)] *)
+ let evars_to_vmcast sigma (emap, c) =
+-  let emap = nf_evars emap in
++  let emap = nf_evar_map emap in
+   let change_exist evar =
+     let ty = Reductionops.nf_betaiota emap (Evd.existential_type emap evar) in
+     mkCast (mkApp (Lazy.force coq_refl_equal,
+@@ -717,7 +717,7 @@ let gappa_internal gl =
+ (** {1 Packaging for [gappa_prepare; gappa_internal]: the [gappa] tactic} *)
+ let gappa_prepare =
+   let id = Ident (dummy_loc, id_of_string "gappa_prepare") in
+-  lazy (Tacinterp.interp (Tacexpr.TacArg (Tacexpr.Reference id)))
++  lazy (Tacinterp.interp (Tacexpr.TacArg (dummy_loc, Tacexpr.Reference id)))
+ 
+ let gappa gl =
+   Coqlib.check_required_library ["Gappa"; "Gappa_tactic"];
+--- ./src/Gappa_round.v.orig	2011-12-08 03:17:56.000000000 -0700
++++ ./src/Gappa_round.v	2012-08-22 16:57:48.106641575 -0600
+@@ -395,7 +395,7 @@ now apply Rlt_not_eq.
+ revert H1.
+ case rdir.
+ intros H1.
+-rewrite Nnat.Z_of_N_succ.
++rewrite N2Z.inj_succ.
+ rewrite Z_of_N_ZtoN.
+ apply sym_eq.
+ apply Zceil_floor_neq.
+--- ./src/Gappa_float.v.orig	2011-12-27 15:10:54.000000000 -0700
++++ ./src/Gappa_float.v	2012-08-22 16:57:48.112641551 -0600
+@@ -526,7 +526,7 @@ simpl (iter_nat (S (nat_of_P p)) positiv
+ rewrite Zpos_xO.
+ rewrite Zpos_xI.
+ ring.
+-rewrite Zneg_plus_distr.
++rewrite <- Pos2Z.add_neg_neg.
+ rewrite <- (Zopp_neg p).
+ ring.
+ apply Rplus_le_reg_r with (Rabs x).
+--- ./src/Gappa_tactic.v.orig	2011-12-16 11:33:27.000000000 -0700
++++ ./src/Gappa_tactic.v	2012-08-22 16:58:28.845476556 -0600
+@@ -567,7 +567,7 @@ destruct o ; try exact H.
+ destruct v as [v|v|v w|v w|o v|o v w|v|v|v|v|v|v|f v] ; try exact H.
+ destruct o ; try exact H.
+ case_eq (RExpr_beq y v) ; intros Hb.
+-rewrite <- RExpr_dec_bl with (1 := Hb).
++rewrite <- internal_RExpr_dec_bl with (1 := Hb).
+ 2: now rewrite Hb in H.
+ simpl.
+ apply <- change_rel_aux.
+@@ -609,7 +609,7 @@ rewrite Gappa_dyadic.Fopp2_correct.
+ apply -> change_rel_aux.
+ split.
+ now apply (Gappa_dyadic.Fpos0_correct (Float2 (Zpos m) e)).
+-rewrite <- RExpr_dec_bl with (1 := Hb) in H.
++rewrite <- internal_RExpr_dec_bl with (1 := Hb) in H.
+ simpl in H1.
+ now rewrite H1.
+ Qed.
+@@ -797,7 +797,7 @@ change (convert_goal_aux gc gh).
+ destruct a as [l' v u'|v w l' u'|v w|v w|] ; try (apply IHgh ; try apply H ; easy).
+ simpl in H.
+ case_eq (RExpr_beq e v) ; intros H3 ; rewrite H3 in H.
+-rewrite (RExpr_dec_bl _ _ H3) in H1, IHgh.
++rewrite (internal_RExpr_dec_bl _ _ H3) in H1, IHgh.
+ generalize (Gminmax_correct _ _ _ _ _ H1 H2).
+ destruct (Gmax_lower l l') as [l''|].
+ destruct (Gmin_upper u u') as [u''|].
diff --git a/gappalib-coq.spec b/gappalib-coq.spec
index cdfc76a..ceb0e94 100644
--- a/gappalib-coq.spec
+++ b/gappalib-coq.spec
@@ -18,6 +18,8 @@ Group:          Applications/Engineering
 License:        LGPLv2+
 URL:            http://gappa.gforge.inria.fr/
 Source0:        https://gforge.inria.fr/frs/download.php/30081/%{name}-%{version}.tar.gz
+# Adapt to changes in coq 8.4.  Sent upstream 22 Aug 2012.
+Patch0:         %{name}-coq84.patch
 
 BuildRequires:  coq%{?_isa} = %{coqver}
 BuildRequires:  flocq
@@ -53,9 +55,7 @@ informational purposes.
 
 %prep
 %setup -q
-
-# Adapt to changes in coq 8.4
-sed -i 's/nf_evars/nf_evar_map/' src/gappatac.ml
+%patch0
 
 %build
 # The %%configure macro specifies --libdir, which this configure script