Commit 6f2f4da9 authored by Heiko Becker's avatar Heiko Becker

Merge branch 'coq8.8_compat' into 'master'

Make FloVer coq 8.8.0 compatible and update CI

See merge request AVA/FloVer!5
parents b1774cab 41d309cc
......@@ -113,7 +113,7 @@ Fixpoint bstep_valid f E :=
Definition bpowQ (r:radix) (e: Z) :=
match e with
|0%Z => 1%Q
| (' p)%Z => (Z.pow_pos r p) #1
| Zpos p => (Z.pow_pos r p) #1
| Z.neg p => Qinv ((Z.pow_pos r p)#1)
end.
......@@ -127,7 +127,7 @@ Definition B2Q :=
| B754_infinity _ _ _ => (bpowQ radix2 emax) +1%Q
| B754_nan _ _ _ _ => (bpowQ radix2 emax) +1%Q
| B754_finite _ _ s m e _ =>
let f_new: Fcore_defs.float radix2 := {| Fcore_defs.Fnum := cond_Zopp s (' m); Fcore_defs.Fexp := e |} in
let f_new: Fcore_defs.float radix2 := {| Fcore_defs.Fnum := cond_Zopp s (Zpos m); Fcore_defs.Fexp := e |} in
(Fcore_defs.Fnum f_new # 1) * bpowQ radix2 (Fcore_defs.Fexp f_new)
end.
......@@ -144,7 +144,7 @@ Proof.
f_equal.
- unfold Z2R, Q2R.
simpl. rewrite RMicromega.Rinv_1.
destruct (cond_Zopp b (' m)); unfold IZR;
destruct (cond_Zopp b (Zpos m)); unfold IZR;
try rewrite P2R_INR, INR_IPR; lra.
- unfold Q2R; simpl.
unfold bpow, bpowQ.
......
......@@ -69,12 +69,12 @@ Lemma Qeq_bool_sym a b:
Qeq_bool a b = Qeq_bool b a.
Proof.
unfold Qeq_bool.
case_eq (Zeq_bool (Qnum a * ' Qden b) (Qnum b * ' Qden a)); intros.
case_eq (Zeq_bool (Qnum a * (Zpos (Qden b))) (Qnum b * (Zpos (Qden a)))); intros.
- rewrite <- Zeq_is_eq_bool in H.
rewrite H; symmetry.
rewrite <- Zeq_is_eq_bool; auto.
- apply Zeq_bool_neq in H.
case_eq (Zeq_bool (Qnum b *' Qden a) (Qnum a * ' Qden b)); intros.
case_eq (Zeq_bool (Qnum b * Zpos (Qden a)) (Qnum a * Zpos (Qden b))); intros.
+ apply Zeq_is_eq_bool in H0.
rewrite H0 in H; auto.
+ auto.
......
......@@ -10,7 +10,7 @@ make -j
make clean
#opam switch coq8.8
#eval `opam config env`
#./configure_coq.sh
#make -j
opam switch coq8.8
eval `opam config env`
./configure_coq.sh
make -j
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment