diff options
| author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2020-09-08 18:29:00 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-04-25 16:38:45 +0200 |
| commit | 9aacc59135071a979623ab177819cdbe9ce27056 (patch) | |
| tree | 1d2069eba895833fdb3a7647c3cc37cea32a0de6 /flocq/Calc/Sqrt.v | |
| parent | fb1f4545dfe861ff4d02816e295021a7e3061687 (diff) | |
| download | compcert-9aacc59135071a979623ab177819cdbe9ce27056.tar.gz compcert-9aacc59135071a979623ab177819cdbe9ce27056.zip | |
Upgrade to Flocq 4.0.
Diffstat (limited to 'flocq/Calc/Sqrt.v')
| -rw-r--r-- | flocq/Calc/Sqrt.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/flocq/Calc/Sqrt.v b/flocq/Calc/Sqrt.v index 4d267d21..3c885bba 100644 --- a/flocq/Calc/Sqrt.v +++ b/flocq/Calc/Sqrt.v @@ -19,8 +19,9 @@ COPYING file for more details. (** * Helper functions and theorems for computing the rounded square root of a floating-point number. *) -From Coq Require Import Lia. -Require Import Raux Defs Digits Generic_fmt Float_prop Bracket. +From Coq Require Import ZArith Reals Lia. + +Require Import Zaux Raux Defs Digits Generic_fmt Float_prop Bracket. Set Implicit Arguments. Set Strongly Strict Implicit. |