diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2022-04-29 09:32:44 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2022-04-29 09:32:44 +0200 |
| commit | 4920f93e4f933c8616a3376da5264d63bd58afdc (patch) | |
| tree | f05cdd8084fcbc2098bbad14dc5b3fe38bf34ba4 /flocq/Prop/Sterbenz.v | |
| parent | fb1f4545dfe861ff4d02816e295021a7e3061687 (diff) | |
| parent | e8c312eecf96ae1703f7ba0b65f107233d340238 (diff) | |
| download | compcert-4920f93e4f933c8616a3376da5264d63bd58afdc.tar.gz compcert-4920f93e4f933c8616a3376da5264d63bd58afdc.zip | |
Merge pull request #368 from silene/flocq-3.4
Upgrade to Flocq 4.1.
Diffstat (limited to 'flocq/Prop/Sterbenz.v')
| -rw-r--r-- | flocq/Prop/Sterbenz.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/flocq/Prop/Sterbenz.v b/flocq/Prop/Sterbenz.v index 9594ac5d..8f516d0e 100644 --- a/flocq/Prop/Sterbenz.v +++ b/flocq/Prop/Sterbenz.v @@ -19,7 +19,9 @@ COPYING file for more details. (** * Sterbenz conditions for exact subtraction *) -Require Import Raux Defs Generic_fmt Operations. +From Coq Require Import ZArith Reals. + +Require Import Zaux Raux Defs Generic_fmt Operations. Section Fprop_Sterbenz. |