Merge PR coq#17899: Add a file to spot-check the specs of primitive f…

…loats Reviewed-by: proux01 Co-authored-by: proux01 <[email protected]>
SkySkimmer · Nov 24, 2023 · 8d0d547 · 8d0d547
2 parents fbb29fa + cd667e4
commit 8d0d547
Show file tree

Hide file tree

Showing 16 changed files with 735 additions and 959 deletions.
diff --git a/test-suite/primitive/float/add.v b/test-suite/primitive/float/add.v
diff --git a/test-suite/primitive/float/classify.v b/test-suite/primitive/float/classify.v
@@ -11,23 +11,3 @@ Check (eq_refl : classify neg_zero = NZero).
 Check (eq_refl : classify infinity = PInf).
 Check (eq_refl : classify neg_infinity = NInf).
 Check (eq_refl : classify nan = NaN).
-
-Check (eq_refl PNormal <: classify one = PNormal).
-Check (eq_refl NNormal <: classify (- one)%float = NNormal).
-Check (eq_refl PSubn <: classify epsilon = PSubn).
-Check (eq_refl NSubn <: classify (- epsilon)%float = NSubn).
-Check (eq_refl PZero <: classify zero = PZero).
-Check (eq_refl NZero <: classify neg_zero = NZero).
-Check (eq_refl PInf <: classify infinity = PInf).
-Check (eq_refl NInf <: classify neg_infinity = NInf).
-Check (eq_refl NaN <: classify nan = NaN).
-
-Check (eq_refl PNormal <<: classify one = PNormal).
-Check (eq_refl NNormal <<: classify (- one)%float = NNormal).
-Check (eq_refl PSubn <<: classify epsilon = PSubn).
-Check (eq_refl NSubn <<: classify (- epsilon)%float = NSubn).
-Check (eq_refl PZero <<: classify zero = PZero).
-Check (eq_refl NZero <<: classify neg_zero = NZero).
-Check (eq_refl PInf <<: classify infinity = PInf).
-Check (eq_refl NInf <<: classify neg_infinity = NInf).
-Check (eq_refl NaN <<: classify nan = NaN).