1 files changed, 0 insertions, 71 deletions
diff --git a/sci-mathematics/gappalib-coq/files/gappalib-coq-coq84.patch b/sci-mathematics/gappalib-coq/files/gappalib-coq-coq84.patch
deleted file mode 100644
index 8a6d07447..000000000
--- a/sci-mathematics/gappalib-coq/files/gappalib-coq-coq84.patch
+++ /dev/null
@@ -1,71 +0,0 @@
---- ./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''|].