Commit 0810e3f1 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Avoid warnings about Require.

parent db356aa5
......@@ -5,6 +5,7 @@ Require Import Fcore_defs.
Require Import Fcore_generic_fmt.
Require Import Fcalc_ops.
Require Import Fcore_ulp.
Require Fcore_FLX Fcore_FLT Fcore_FTZ.
Require Import Fappli_double_round.
......@@ -837,7 +838,7 @@ Qed.
Section Double_round_mult_beta_odd_FLX.
Require Import Fcore_FLX.
Import Fcore_FLX.
Variable prec : Z.
Variable prec' : Z.
......@@ -865,8 +866,8 @@ End Double_round_mult_beta_odd_FLX.
Section Double_round_mult_beta_odd_FLT.
Require Import Fcore_FLX.
Require Import Fcore_FLT.
Import Fcore_FLX.
Import Fcore_FLT.
Variable emin prec : Z.
Variable emin' prec' : Z.
......@@ -898,7 +899,8 @@ End Double_round_mult_beta_odd_FLT.
Section Double_round_mult_beta_odd_FTZ.
Require Import Fcore_FTZ.
Import Fcore_FLX.
Import Fcore_FTZ.
Variable emin prec : Z.
Variable emin' prec' : Z.
......@@ -1170,7 +1172,7 @@ Qed.
Section Double_round_plus_beta_odd_FLX.
Require Import Fcore_FLX.
Import Fcore_FLX.
Variable prec : Z.
Variable prec' : Z.
......@@ -1214,8 +1216,8 @@ End Double_round_plus_beta_odd_FLX.
Section Double_round_plus_beta_odd_FLT.
Require Import Fcore_FLX.
Require Import Fcore_FLT.
Import Fcore_FLX.
Import Fcore_FLT.
Variable emin prec : Z.
Variable emin' prec' : Z.
......@@ -1267,7 +1269,8 @@ End Double_round_plus_beta_odd_FLT.
Section Double_round_plus_beta_odd_FTZ.
Require Import Fcore_FTZ.
Import Fcore_FLX.
Import Fcore_FTZ.
Variable emin prec : Z.
Variable emin' prec' : Z.
......@@ -1548,7 +1551,7 @@ Qed.
Section Double_round_sqrt_beta_odd_FLX.
Require Import Fcore_FLX.
Import Fcore_FLX.
Variable prec : Z.
Variable prec' : Z.
......@@ -1575,8 +1578,8 @@ End Double_round_sqrt_beta_odd_FLX.
Section Double_round_sqrt_beta_odd_FLT.
Require Import Fcore_FLX.
Require Import Fcore_FLT.
Import Fcore_FLX.
Import Fcore_FLT.
Variable emin prec : Z.
Variable emin' prec' : Z.
......@@ -1607,7 +1610,8 @@ End Double_round_sqrt_beta_odd_FLT.
Section Double_round_sqrt_beta_odd_FTZ.
Require Import Fcore_FTZ.
Import Fcore_FLX.
Import Fcore_FTZ.
Variable emin prec : Z.
Variable emin' prec' : Z.
......@@ -2276,7 +2280,7 @@ Qed.
Section Double_round_div_beta_odd_rna_FLX.
Require Import Fcore_FLX.
Import Fcore_FLX.
Variable prec : Z.
Variable prec' : Z.
......@@ -2307,8 +2311,8 @@ End Double_round_div_beta_odd_rna_FLX.
Section Double_round_div_beta_odd_rna_FLT.
Require Import Fcore_FLX.
Require Import Fcore_FLT.
Import Fcore_FLX.
Import Fcore_FLT.
Variable emin prec : Z.
Variable emin' prec' : Z.
......@@ -2343,8 +2347,8 @@ End Double_round_div_beta_odd_rna_FLT.
Section Double_round_div_beta_odd_rna_FTZ.
Require Import Fcore_FLX.
Require Import Fcore_FTZ.
Import Fcore_FLX.
Import Fcore_FTZ.
Variable emin prec : Z.
Variable emin' prec' : Z.
......
......@@ -5,6 +5,7 @@ Require Import Fcore_defs.
Require Import Fcore_generic_fmt.
Require Import Fcalc_ops.
Require Import Fcore_ulp.
Require Fcore_FLX Fcore_FLT Fcore_FTZ.
Require Import Psatz.
......@@ -659,7 +660,7 @@ Qed.
Section Double_round_mult_FLX.
Require Import Fcore_FLX.
Import Fcore_FLX.
Variable prec : Z.
Variable prec' : Z.
......@@ -685,8 +686,8 @@ End Double_round_mult_FLX.
Section Double_round_mult_FLT.
Require Import Fcore_FLX.
Require Import Fcore_FLT.
Import Fcore_FLX.
Import Fcore_FLT.
Variable emin prec : Z.
Variable emin' prec' : Z.
......@@ -718,7 +719,8 @@ End Double_round_mult_FLT.
Section Double_round_mult_FTZ.
Require Import Fcore_FTZ.
Import Fcore_FLX.
Import Fcore_FTZ.
Variable emin prec : Z.
Variable emin' prec' : Z.
......@@ -1611,7 +1613,7 @@ Qed.
Section Double_round_plus_FLX.
Require Import Fcore_FLX.
Import Fcore_FLX.
Variable prec : Z.
Variable prec' : Z.
......@@ -1667,8 +1669,8 @@ End Double_round_plus_FLX.
Section Double_round_plus_FLT.
Require Import Fcore_FLX.
Require Import Fcore_FLT.
Import Fcore_FLX.
Import Fcore_FLT.
Variable emin prec : Z.
Variable emin' prec' : Z.
......@@ -1739,8 +1741,8 @@ End Double_round_plus_FLT.
Section Double_round_plus_FTZ.
Require Import Fcore_FLX.
Require Import Fcore_FTZ.
Import Fcore_FLX.
Import Fcore_FTZ.
Variable emin prec : Z.
Variable emin' prec' : Z.
......@@ -2325,7 +2327,7 @@ Qed.
Section Double_round_plus_beta_ge_3_FLX.
Require Import Fcore_FLX.
Import Fcore_FLX.
Variable prec : Z.
Variable prec' : Z.
......@@ -2385,8 +2387,8 @@ End Double_round_plus_beta_ge_3_FLX.
Section Double_round_plus_beta_ge_3_FLT.
Require Import Fcore_FLX.
Require Import Fcore_FLT.
Import Fcore_FLX.
Import Fcore_FLT.
Variable emin prec : Z.
Variable emin' prec' : Z.
......@@ -2461,8 +2463,8 @@ End Double_round_plus_beta_ge_3_FLT.
Section Double_round_plus_beta_ge_3_FTZ.
Require Import Fcore_FLX.
Require Import Fcore_FTZ.
Import Fcore_FLX.
Import Fcore_FTZ.
Variable emin prec : Z.
Variable emin' prec' : Z.
......@@ -2880,7 +2882,7 @@ Qed.
Section Double_round_sqrt_FLX.
Require Import Fcore_FLX.
Import Fcore_FLX.
Variable prec : Z.
Variable prec' : Z.
......@@ -2917,8 +2919,8 @@ End Double_round_sqrt_FLX.
Section Double_round_sqrt_FLT.
Require Import Fcore_FLX.
Require Import Fcore_FLT.
Import Fcore_FLX.
Import Fcore_FLT.
Variable emin prec : Z.
Variable emin' prec' : Z.
......@@ -2972,8 +2974,8 @@ End Double_round_sqrt_FLT.
Section Double_round_sqrt_FTZ.
Require Import Fcore_FLX.
Require Import Fcore_FTZ.
Import Fcore_FLX.
Import Fcore_FTZ.
Variable emin prec : Z.
Variable emin' prec' : Z.
......@@ -3318,7 +3320,7 @@ Qed.
Section Double_round_sqrt_beta_ge_4_FLX.
Require Import Fcore_FLX.
Import Fcore_FLX.
Variable prec : Z.
Variable prec' : Z.
......@@ -3357,8 +3359,8 @@ End Double_round_sqrt_beta_ge_4_FLX.
Section Double_round_sqrt_beta_ge_4_FLT.
Require Import Fcore_FLX.
Require Import Fcore_FLT.
Import Fcore_FLX.
Import Fcore_FLT.
Variable emin prec : Z.
Variable emin' prec' : Z.
......@@ -3414,8 +3416,8 @@ End Double_round_sqrt_beta_ge_4_FLT.
Section Double_round_sqrt_beta_ge_4_FTZ.
Require Import Fcore_FLX.
Require Import Fcore_FTZ.
Import Fcore_FLX.
Import Fcore_FTZ.
Variable emin prec : Z.
Variable emin' prec' : Z.
......@@ -4401,7 +4403,7 @@ Qed.
Section Double_round_div_FLX.
Require Import Fcore_FLX.
Import Fcore_FLX.
Variable prec : Z.
Variable prec' : Z.
......@@ -4445,8 +4447,8 @@ End Double_round_div_FLX.
Section Double_round_div_FLT.
Require Import Fcore_FLX.
Require Import Fcore_FLT.
Import Fcore_FLX.
Import Fcore_FLT.
Variable emin prec : Z.
Variable emin' prec' : Z.
......@@ -4515,8 +4517,8 @@ End Double_round_div_FLT.
Section Double_round_div_FTZ.
Require Import Fcore_FLX.
Require Import Fcore_FTZ.
Import Fcore_FLX.
Import Fcore_FTZ.
Variable emin prec : Z.
Variable emin' prec' : Z.
......
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