Commit 24cf49f7 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Reduced dependencies of Fprop_Sterbenz.

parent 948f1e3b
...@@ -18,7 +18,10 @@ COPYING file for more details. ...@@ -18,7 +18,10 @@ COPYING file for more details.
*) *)
(** * Sterbenz conditions for exact subtraction *) (** * Sterbenz conditions for exact subtraction *)
Require Import Fcore.
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_generic_fmt.
Require Import Fcalc_ops. Require Import Fcalc_ops.
Section Fprop_Sterbenz. Section Fprop_Sterbenz.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment