Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project
Project
Details
Activity
Releases
Cycle Analytics
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Issues
59
Issues
59
List
Board
Labels
Milestones
Merge Requests
7
Merge Requests
7
Registry
Registry
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Charts
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
403a0f08
Commit
403a0f08
authored
Feb 16, 2015
by
Guillaume Melquiond
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Make GenFloat.v compatible with Coq 8.5.
parent
dc4c0616
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
8 additions
and
8 deletions
+8
-8
configure.in
configure.in
+1
-1
GenFloat.v
lib/coq/floating_point/GenFloat.v
+7
-7
No files found.
configure.in
View file @
403a0f08
...
...
@@ -543,7 +543,7 @@ fi
if test "$enable_coq_libs" = yes; then
AC_MSG_CHECKING([for Flocq])
AS_IF(
[ echo "Require Import Flocq_version BinNat." \
[ echo "Require Import Flocq
.Flocq
_version BinNat." \
"Goal (20200 <= Flocq_version)%N. easy. Qed." > conftest.v
"$COQC" conftest.v > conftest.err ],
[ AC_MSG_RESULT(yes) ],
...
...
lib/coq/floating_point/GenFloat.v
View file @
403a0f08
...
...
@@ -10,8 +10,8 @@ Require real.Abs.
Require
real
.
FromInt
.
Require
floating_point
.
Rounding
.
Require
Import
Fcore
.
Require
Import
Fappli_IEEE
.
Require
Import
F
locq
.
Core
.
F
core
.
Require
Import
F
locq
.
Appli
.
F
appli_IEEE
.
Require
Import
int
.
Abs
.
Section
GenFloat
.
...
...
@@ -82,7 +82,7 @@ intros H _ _.
now
injection
H
.
clear
.
destruct
(
Bool
.
bool_dec
xs
ys
)
as
[
->|
Hs
]
.
destruct
(
Z_eq_dec
(
Zpos
(
proj
T1
xm
'
))
(
Zpos
(
projT1
ym
'
)))
as
[
Hm
'
|
Hm
'
]
.
destruct
(
Z_eq_dec
(
Zpos
(
proj
1_sig
xm
'
))
(
Zpos
(
proj1_sig
ym
'
)))
as
[
Hm
'
|
Hm
'
]
.
left
.
apply
f_equal3
;
try
easy
.
apply
f_equal2
;
try
easy
.
...
...
@@ -293,7 +293,7 @@ apply generic_format_abs.
apply
generic_format_B2R
.
apply
generic_format_bpow
.
unfold
FLT_exp
,
emin
.
clear
;
zify
;
generalize
Hprec
'
Hemax
'
;
omega
.
zify
;
generalize
Hprec
'
Hemax
'
;
omega
.
apply
bpow_gt_0
.
apply
abs_B2R_lt_emax
.
unfold
pred
.
...
...
@@ -310,7 +310,7 @@ rewrite Z2R_minus, Z2R_Zpower.
simpl
;
ring
.
apply
Zlt_le_weak
.
exact
Hprec
'
.
clear
;
generalize
Hprec
'
Hemax
'
;
omega
.
generalize
Hprec
'
Hemax
'
;
omega
.
Qed
.
(
*
Why3
goal
*
)
...
...
@@ -335,14 +335,14 @@ split.
rewrite
Z2R_IZR
.
now
rewrite
Rmult_1_r
.
split
.
easy
.
clear
;
unfold
emin
;
generalize
Hprec
'
Hemax
'
;
omega
.
unfold
emin
;
generalize
Hprec
'
Hemax
'
;
omega
.
unfold
max_representable_integer
in
Bz
.
change
2
%
Z
with
(
radix_val
radix2
)
in
Bz
.
apply
generic_format_abs_inv
.
rewrite
<-
Z2R_IZR
,
<-
Z2R_abs
,
Bz
,
Z2R_Zpower
.
apply
generic_format_bpow
.
unfold
FLT_exp
,
emin
.
clear
;
generalize
Hprec
'
Hemax
'
;
zify
.
clear
Bz
;
generalize
Hprec
'
Hemax
'
;
zify
.
omega
.
apply
Zlt_le_weak
.
apply
Hprec
'
.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment