Commit eaa9655d authored by Guillaume Melquiond's avatar Guillaume Melquiond

Ensure compatibility with Coq 8.5.

parent f5709f0c
Require Import Reals Fcore.
Require Import Gappa_tactic Interval_tactic.
Require Import Gappa.Gappa_tactic Interval.Interval_tactic.
Open Scope R_scope.
......
......@@ -35,7 +35,7 @@ now apply F2R_ge_0_compat.
Qed.
Definition plus (x y : float beta) :=
let '(Float m e) := Fplus beta x y in
let (m, e) := Fplus beta x y in
let s := Zlt_bool m 0 in
let '(m', e', l) := truncate beta fexp (Zabs m, e, loc_Exact) in
Float beta (cond_Zopp s (choice s m' l)) e'.
......@@ -58,7 +58,7 @@ apply sym_eq, F2R_Zabs.
Qed.
Definition mult (x y : float beta) :=
let '(Float m e) := Fmult beta x y in
let (m, e) := Fmult beta x y in
let s := Zlt_bool m 0 in
let '(m', e', l) := truncate beta fexp (Zabs m, e, loc_Exact) in
Float beta (cond_Zopp s (choice s m' l)) e'.
......@@ -81,7 +81,7 @@ apply sym_eq, F2R_Zabs.
Qed.
Definition sqrt (x : float beta) :=
let '(Float m e) := x in
let (m, e) := x in
if Zlt_bool 0 m then
let '(m', e', l) := truncate beta fexp (Fsqrt_core beta prec m e) in
Float beta (choice false m' l) e'
......@@ -162,8 +162,8 @@ now elim Hy0.
Qed.
Definition div (x y : float beta) :=
let '(Float mx ex) := x in
let '(Float my ey) := y in
let (mx, ex) := x in
let (my, ey) := y in
if Zeq_bool mx 0 then Float beta 0 0
else
let '(m, e, l) := truncate beta fexp (Fdiv_core beta prec (Zabs mx) ex (Zabs my) ey) in
......
Require Import Reals Psatz.
Require Import Fcore Gappa_tactic.
Require Import Fcore Gappa.Gappa_tactic.
Open Scope R_scope.
......
Require Import Fcore.
Require Import Interval_tactic.
Require Import Interval.Interval_tactic.
Section Sec1.
......
......@@ -3,7 +3,7 @@ Require Import Fcore.
Require Import Fprop_relative.
Require Import Fprop_Sterbenz.
Require Import Fcalc_ops.
Require Import Interval_tactic.
Require Import Interval.Interval_tactic.
Section Delta_FLX.
Open Scope R_scope.
......
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