diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-24 22:39:55 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-24 22:39:55 +0100 |
| commit | 2bbe86d4efe2ae08444359008798c12adf0c9b60 (patch) | |
| tree | 828a32ea1b98c3682902f63d0ed85a9ba24351de /kvx | |
| parent | 0ec09c99af2071f52271dd5e14846f5da3bcb718 (diff) | |
| download | compcert-kvx-2bbe86d4efe2ae08444359008798c12adf0c9b60.tar.gz compcert-kvx-2bbe86d4efe2ae08444359008798c12adf0c9b60.zip | |
some progress
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/FPDivision64.v | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index e4f883e7..3685f601 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -1428,7 +1428,6 @@ Proof. replace (ZnearestE q' + -1)%Z with (ZnearestE q' - 1)%Z by ring. set (q'' := (ZnearestE q')) in *. - Check Int64.sub_signed. fold a'. rewrite int64_mul_signed_unsigned. rewrite q_SIGNED. @@ -1706,7 +1705,6 @@ Proof. replace (ZnearestE q' + -1)%Z with (ZnearestE q' - 1)%Z by ring. set (q'' := (ZnearestE q')) in *. - Check Int64.sub_signed. fold a'. rewrite int64_mul_signed_unsigned. rewrite q_SIGNED. |