From 04e22abe4378e29671def7b4d9c7e509c58ef6b6 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Tue, 31 Mar 2020 19:12:18 +0200
Subject: [primitive floats] Add low level hexadecimal printing

---
 test-suite/output/FloatSyntax.v | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'test-suite/output/FloatSyntax.v')

diff --git a/test-suite/output/FloatSyntax.v b/test-suite/output/FloatSyntax.v
index 36ffc27239..d3eb6d2e4c 100644
--- a/test-suite/output/FloatSyntax.v
+++ b/test-suite/output/FloatSyntax.v
@@ -30,6 +30,15 @@ Check -0xb.2cp-2.
 Check 1e309.
 Check -1e309.
 
+Set Printing All.
+Check 0.5.
+Unset Printing All.
+Check 0.5.
+Unset Printing Float.
+Check 0.5.
+Set Printing Float.
+Check 0.5.
+
 Open Scope nat_scope.
 
 Check 2.
-- 
cgit v1.2.3