2 files changed, 74 insertions, 0 deletions
diff --git a/test-suite/output/FloatSyntax.out b/test-suite/output/FloatSyntax.out
new file mode 100644
index 0000000000..f67119020e
--- /dev/null
+++ b/test-suite/output/FloatSyntax.out
@@ -0,0 +1,40 @@
+2%float
+     : float
+2.5%float
+     : float
+(-2.5)%float
+     : float
+2.5e+20%float
+     : float
+(-2.4999999999999999e-20)%float
+     : float
+(2 + 2)%float
+     : float
+(2.5 + 2.5)%float
+     : float
+2
+     : float
+2.5
+     : float
+-2.5
+     : float
+2.5e+20
+     : float
+-2.4999999999999999e-20
+     : float
+2 + 2
+     : float
+2.5 + 2.5
+     : float
+2
+     : nat
+2%float
+     : float
+t = 2%flt
+     : float
+t = 2%flt
+     : float
+2
+     : nat
+2
+     : float
diff --git a/test-suite/output/FloatSyntax.v b/test-suite/output/FloatSyntax.v
new file mode 100644
index 0000000000..1caa0bb444
--- /dev/null
+++ b/test-suite/output/FloatSyntax.v
@@ -0,0 +1,34 @@
+Require Import Floats.
+
+Check 2%float.
+Check 2.5%float.
+Check (-2.5)%float.
+Check 2.5e20%float.
+Check (-2.5e-20)%float.
+Check (2 + 2)%float.
+Check (2.5 + 2.5)%float.
+
+Open Scope float_scope.
+
+Check 2.
+Check 2.5.
+Check (-2.5).
+Check 2.5e20.
+Check (-2.5e-20).
+Check (2 + 2).
+Check (2.5 + 2.5).
+
+Open Scope nat_scope.
+
+Check 2.
+Check 2%float.
+
+Delimit Scope float_scope with flt.
+Definition t := 2%float.
+Print t.
+Delimit Scope nat_scope with float.
+Print t.
+Check 2.
+Close Scope nat_scope.
+Check 2.
+Close Scope float_scope.