6 files changed, 104 insertions, 22 deletions
diff --git a/test-suite/output/FloatExtraction.out b/test-suite/output/FloatExtraction.out
index dd8189c56f..539ec9b2bf 100644
--- a/test-suite/output/FloatExtraction.out
+++ b/test-suite/output/FloatExtraction.out
@@ -1,16 +1,18 @@
 File "stdin", line 25, characters 8-12:
 Warning: The constant 0.01 is not a binary64 floating-point value. A closest
-value will be used and unambiguously printed 0.01. [inexact-float,parsing]
+value 0x1.47ae147ae147bp-7 will be used and unambiguously printed 0.01.
+[inexact-float,parsing]
 File "stdin", line 25, characters 20-25:
 Warning: The constant -0.01 is not a binary64 floating-point value. A closest
-value will be used and unambiguously printed -0.01. [inexact-float,parsing]
+value -0x1.47ae147ae147bp-7 will be used and unambiguously printed -0.01.
+[inexact-float,parsing]
 File "stdin", line 25, characters 27-35:
 Warning: The constant 1.7e+308 is not a binary64 floating-point value. A
-closest value will be used and unambiguously printed 1.6999999999999999e+308.
-[inexact-float,parsing]
+closest value 0x1.e42d130773b76p+1023 will be used and unambiguously printed
+1.6999999999999999e+308. [inexact-float,parsing]
 File "stdin", line 25, characters 37-46:
 Warning: The constant -1.7e-308 is not a binary64 floating-point value. A
-closest value will be used and unambiguously printed
+closest value -0x0.c396c98f8d899p-1022 will be used and unambiguously printed
 -1.7000000000000002e-308. [inexact-float,parsing]
 
 (** val infinity : Float64.t **)
diff --git a/test-suite/output/FloatSyntax.out b/test-suite/output/FloatSyntax.out
index 4a5a700879..0b18e9a3d2 100644
--- a/test-suite/output/FloatSyntax.out
+++ b/test-suite/output/FloatSyntax.out
@@ -6,13 +6,13 @@
      : float
 File "stdin", line 9, characters 6-13:
 Warning: The constant 2.5e123 is not a binary64 floating-point value. A
-closest value will be used and unambiguously printed 2.4999999999999999e+123.
-[inexact-float,parsing]
+closest value 0x1.e412f0f768fadp+409 will be used and unambiguously printed
+2.4999999999999999e+123. [inexact-float,parsing]
 2.4999999999999999e+123%float
      : float
 File "stdin", line 10, characters 7-16:
 Warning: The constant -2.5e-123 is not a binary64 floating-point value. A
-closest value will be used and unambiguously printed
+closest value -0x1.a71368f0f3047p-408 will be used and unambiguously printed
 -2.5000000000000001e-123. [inexact-float,parsing]
 (-2.5000000000000001e-123)%float
      : float
@@ -28,13 +28,13 @@ closest value will be used and unambiguously printed
      : float
 File "stdin", line 19, characters 6-13:
 Warning: The constant 2.5e123 is not a binary64 floating-point value. A
-closest value will be used and unambiguously printed 2.4999999999999999e+123.
-[inexact-float,parsing]
+closest value 0x1.e412f0f768fadp+409 will be used and unambiguously printed
+2.4999999999999999e+123. [inexact-float,parsing]
 2.4999999999999999e+123
      : float
 File "stdin", line 20, characters 7-16:
 Warning: The constant -2.5e-123 is not a binary64 floating-point value. A
-closest value will be used and unambiguously printed
+closest value -0x1.a71368f0f3047p-408 will be used and unambiguously printed
 -2.5000000000000001e-123. [inexact-float,parsing]
 -2.5000000000000001e-123
      : float
@@ -56,16 +56,24 @@ closest value will be used and unambiguously printed
      : float
 File "stdin", line 30, characters 6-11:
 Warning: The constant 1e309 is not a binary64 floating-point value. A closest
-value will be used and unambiguously printed infinity.
+value infinity will be used and unambiguously printed infinity.
 [inexact-float,parsing]
 infinity
      : float
 File "stdin", line 31, characters 6-12:
 Warning: The constant -1e309 is not a binary64 floating-point value. A
-closest value will be used and unambiguously printed neg_infinity.
-[inexact-float,parsing]
+closest value neg_infinity will be used and unambiguously printed
+neg_infinity. [inexact-float,parsing]
 neg_infinity
      : float
+0x1p-1
+     : float
+0.5
+     : float
+0x1p-1
+     : float
+0.5
+     : float
 2
      : nat
 2%float
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.
diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out
index 190c34262f..ca4858d7a7 100644
--- a/test-suite/output/PrintAssumptions.out
+++ b/test-suite/output/PrintAssumptions.out
@@ -7,17 +7,17 @@ bli : Type
 Axioms:
 bli : Type
 Axioms:
-extensionality : forall (P Q : Type) (f g : P -> Q),
-                 (forall x : P, f x = g x) -> f = g
+extensionality
+  : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g
 Axioms:
-extensionality : forall (P Q : Type) (f g : P -> Q),
-                 (forall x : P, f x = g x) -> f = g
+extensionality
+  : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g
 Axioms:
-extensionality : forall (P Q : Type) (f g : P -> Q),
-                 (forall x : P, f x = g x) -> f = g
+extensionality
+  : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g
 Axioms:
-extensionality : forall (P Q : Type) (f g : P -> Q),
-                 (forall x : P, f x = g x) -> f = g
+extensionality
+  : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g
 Closed under the global context
 Closed under the global context
 Axioms:
diff --git a/test-suite/output/ltac2_notations_eval_in.out b/test-suite/output/ltac2_notations_eval_in.out
new file mode 100644
index 0000000000..15e43b7fb9
--- /dev/null
+++ b/test-suite/output/ltac2_notations_eval_in.out
@@ -0,0 +1,21 @@
+- : constr =
+constr:((fix add (n m : nat) {struct n} : nat :=
+           match n with
+           | 0 => m
+           | S p => S (add p m)
+           end) (1 + 2) 3)
+- : constr = constr:(S (0 + 2 + 3))
+- : constr = constr:(6)
+- : constr = constr:(1 + 2 + 3)
+- : constr = constr:(6)
+- : constr = constr:(1 + 2 + 3)
+- : constr = constr:(1 + 2 + 3)
+- : constr = constr:(6)
+- : constr = constr:(1 + 2 + 3)
+- : constr = constr:(1 + 2 + 3)
+- : constr = constr:(6)
+- : constr = constr:(1 + 2 + 3)
+- : constr = constr:(1 + 2 + 3)
+- : constr list = [constr:(0 <> 0); constr:(0 = 0 -> False);
+constr:((fun P : Prop => P -> False) (0 = 0)); constr:(
+0 <> 0)]
diff --git a/test-suite/output/ltac2_notations_eval_in.v b/test-suite/output/ltac2_notations_eval_in.v
new file mode 100644
index 0000000000..4a11e7cae0
--- /dev/null
+++ b/test-suite/output/ltac2_notations_eval_in.v
@@ -0,0 +1,42 @@
+From Ltac2 Require Import Ltac2.
+From Coq Require Import ZArith.
+
+(** * Test eval ... in / reduction tactics *)
+
+(** The below test cases test if the notation syntax works - not the tactics as such *)
+
+Ltac2 Eval (eval red in (1+2+3)).
+
+Ltac2 Eval (eval hnf in (1+2+3)).
+
+Ltac2 Eval (eval simpl in (1+2+3)).
+
+Ltac2 Eval (eval simpl Z.add in (1+2+3)).
+
+Ltac2 Eval (eval cbv in (1+2+3)).
+
+Ltac2 Eval (eval cbv delta [Z.add] beta iota in (1+2+3)).
+
+Ltac2 Eval (eval cbv delta [Z.add Pos.add] beta iota in (1+2+3)).
+
+Ltac2 Eval (eval cbn in (1+2+3)).
+
+Ltac2 Eval (eval cbn delta [Z.add] beta iota in (1+2+3)).
+
+Ltac2 Eval (eval cbn delta [Z.add Pos.add] beta iota in (1+2+3)).
+
+Ltac2 Eval (eval lazy in (1+2+3)).
+
+Ltac2 Eval (eval lazy delta [Z.add] beta iota in (1+2+3)).
+
+Ltac2 Eval (eval lazy delta [Z.add Pos.add] beta iota in (1+2+3)).
+
+(* The example for [fold] in the reference manual *)
+
+Ltac2 Eval (
+  let t1 := '(~0=0) in
+  let t2 := eval unfold not in $t1 in
+  let t3 := eval pattern (0=0) in $t2 in
+  let t4 := eval fold not in $t3 in
+  [t1; t2; t3; t4]
+).