From 1b0bd3a9e3a913a4928b68546a134a1a4448f9e8 Mon Sep 17 00:00:00 2001
From: Guillaume Bertholon
Date: Mon, 16 Jul 2018 13:30:37 +0200
Subject: Add tests for primitive floats

Add utility ldexp and frexp functions to prevent dealing with the shift of
ldshiftexp and frshiftexp everywhere.

Also move primitive integer tests to place all primitive tests in the
same directory.
---
 test-suite/primitive/float/zero.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/primitive/float/zero.v

(limited to 'test-suite/primitive/float/zero.v')

diff --git a/test-suite/primitive/float/zero.v b/test-suite/primitive/float/zero.v
new file mode 100644
index 0000000000..75348d4657
--- /dev/null
+++ b/test-suite/primitive/float/zero.v
@@ -0,0 +1,7 @@
+Require Import ZArith Int63 Floats.
+
+Open Scope float_scope.
+
+Fail Check (eq_refl : zero = neg_zero).
+Fail Check (eq_refl <: zero = neg_zero).
+Fail Check (eq_refl <<: zero = neg_zero).
-- 
cgit v1.2.3