diff options
author | Yann Herklotz <git@yannherklotz.com> | 2022-03-10 14:13:19 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2022-03-10 14:13:19 +0100 |
commit | 163f4a4e4467f64759dfa67bd555e6b893692561 (patch) | |
tree | 81731eb1f0e6bdc6c1fc321d0b865bb056eef5cc /lib/Floats.v | |
parent | c68661bd1eb5565e1272e039d7c2fa34086abf90 (diff) | |
download | compcert-kvx-vericert.tar.gz compcert-kvx-vericert.zip |
Compile under the name: kvxvericert
Diffstat (limited to 'lib/Floats.v')
-rw-r--r-- | lib/Floats.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/Floats.v b/lib/Floats.v index b10b3392..6530b41c 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -18,7 +18,7 @@ (** Formalization of floating-point numbers, using the Flocq library. *) Require Import Coqlib Zbits Integers Axioms. -From Flocq Require Import Binary Bits Core. +From kvx.Flocq Require Import Binary Bits Core. Require Import IEEE754_extra. Require Import Program. Require Archi. |