7 files changed, 82 insertions, 62 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_010.v b/test-suite/bugs/closed/HoTT_coq_010.v
index 42b1244fb5..caa7373f5e 100644
--- a/test-suite/bugs/closed/HoTT_coq_010.v
+++ b/test-suite/bugs/closed/HoTT_coq_010.v
@@ -1,3 +1,3 @@
-SearchAbout and.
+Search and.
 (* Anomaly: Mismatched instance and context when building universe substitution.
 Please report. *)
diff --git a/test-suite/bugs/closed/bug_3900.v b/test-suite/bugs/closed/bug_3900.v
index 6be2161c2f..ddede74acc 100644
--- a/test-suite/bugs/closed/bug_3900.v
+++ b/test-suite/bugs/closed/bug_3900.v
@@ -9,5 +9,5 @@ Variable Pmor : forall s d : obj, morphism A (projT1 s) (projT1 d) -> Type.
 Class Foo (x : Type) := { _ : forall y, y }.
 Local Instance ishset_pmor {s d m} : Foo (Pmor s d m).
 Proof.
-SearchAbout ((forall _ _, _) -> Foo _).
+Search ((forall _ _, _) -> Foo _).
 Abort.
diff --git a/test-suite/output/FloatExtraction.out b/test-suite/output/FloatExtraction.out
index cfd6633752..dd8189c56f 100644
--- a/test-suite/output/FloatExtraction.out
+++ b/test-suite/output/FloatExtraction.out
@@ -1,3 +1,17 @@
+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]
+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]
+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]
+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
+-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 668a55977d..7941d2e647 100644
--- a/test-suite/output/FloatSyntax.out
+++ b/test-suite/output/FloatSyntax.out
@@ -4,8 +4,16 @@
      : float
 (-2.5)%float
      : 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]
 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
+-2.5000000000000001e-123. [inexact-float,parsing]
 (-2.5000000000000001e-123)%float
      : float
 (2 + 2)%float
@@ -18,14 +26,34 @@
      : float
 -2.5
      : 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]
 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
+-2.5000000000000001e-123. [inexact-float,parsing]
 -2.5000000000000001e-123
      : float
 2 + 2
      : float
 2.5 + 2.5
      : float
+File "stdin", line 24, characters 6-11:
+Warning: The constant 1e309 is not a binary64 floating-point value. A closest
+value will be used and unambiguously printed infinity.
+[inexact-float,parsing]
+infinity
+     : float
+File "stdin", line 25, 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]
+neg_infinity
+     : float
 2
      : nat
 2%float
diff --git a/test-suite/output/FloatSyntax.v b/test-suite/output/FloatSyntax.v
index 85f611352c..eca712db10 100644
--- a/test-suite/output/FloatSyntax.v
+++ b/test-suite/output/FloatSyntax.v
@@ -21,6 +21,9 @@ Check (-2.5e-123).
 Check (2 + 2).
 Check (2.5 + 2.5).
 
+Check 1e309.
+Check -1e309.
+
 Open Scope nat_scope.
 
 Check 2.
diff --git a/test-suite/success/search.v b/test-suite/success/search.v
new file mode 100644
index 0000000000..92de43e052
--- /dev/null
+++ b/test-suite/success/search.v
@@ -0,0 +1,35 @@
+
+(** Test of the different syntaxes of Search *)
+
+Search plus.
+Search plus mult.
+Search "plus_n".
+Search plus "plus_n".
+Search "*".
+Search "*" "+".
+
+Search plus inside Peano.
+Search plus mult inside Peano.
+Search "plus_n" inside Peano.
+Search plus "plus_n" inside Peano.
+Search "*" inside Peano.
+Search "*" "+" inside Peano.
+
+Search plus outside Peano Logic.
+Search plus mult outside Peano Logic.
+Search "plus_n" outside Peano Logic.
+Search plus "plus_n" outside Peano Logic.
+Search "*" outside Peano Logic.
+Search "*" "+" outside Peano Logic.
+
+Search -"*" "+" outside Logic.
+Search -"*"%nat "+"%nat outside Logic.
+
+
+(** The example in the Reference Manual *)
+
+Require Import ZArith.
+
+Search Z.mul Z.add "distr".
+Search "+"%Z "*"%Z "distr" -positive -Prop.
+Search (?x * _ + ?x * _)%Z outside OmegaLemmas.
diff --git a/test-suite/success/searchabout.v b/test-suite/success/searchabout.v
deleted file mode 100644
index 9edfd82556..0000000000
--- a/test-suite/success/searchabout.v
+++ /dev/null
@@ -1,60 +0,0 @@
-
-(** Test of the different syntaxes of SearchAbout, in particular
-    with and without the [ ... ] delimiters *)
-
-SearchAbout plus.
-SearchAbout plus mult.
-SearchAbout "plus_n".
-SearchAbout plus "plus_n".
-SearchAbout "*".
-SearchAbout "*" "+".
-
-SearchAbout plus inside Peano.
-SearchAbout plus mult inside Peano.
-SearchAbout "plus_n" inside Peano.
-SearchAbout plus "plus_n" inside Peano.
-SearchAbout "*" inside Peano.
-SearchAbout "*" "+" inside Peano.
-
-SearchAbout plus outside Peano Logic.
-SearchAbout plus mult outside Peano Logic.
-SearchAbout "plus_n" outside Peano Logic.
-SearchAbout plus "plus_n" outside Peano Logic.
-SearchAbout "*" outside Peano Logic.
-SearchAbout "*" "+" outside Peano Logic.
-
-SearchAbout -"*" "+" outside Logic.
-SearchAbout -"*"%nat "+"%nat outside Logic.
-
-SearchAbout [plus].
-SearchAbout [plus mult].
-SearchAbout ["plus_n"].
-SearchAbout [plus "plus_n"].
-SearchAbout ["*"].
-SearchAbout ["*" "+"].
-
-SearchAbout [plus] inside Peano.
-SearchAbout [plus mult] inside Peano.
-SearchAbout ["plus_n"] inside Peano.
-SearchAbout [plus "plus_n"] inside Peano.
-SearchAbout ["*"] inside Peano.
-SearchAbout ["*" "+"] inside Peano.
-
-SearchAbout [plus] outside Peano Logic.
-SearchAbout [plus mult] outside Peano Logic.
-SearchAbout ["plus_n"] outside Peano Logic.
-SearchAbout [plus "plus_n"] outside Peano Logic.
-SearchAbout ["*"] outside Peano Logic.
-SearchAbout ["*" "+"] outside Peano Logic.
-
-SearchAbout [-"*" "+"] outside Logic.
-SearchAbout [-"*"%nat "+"%nat] outside Logic.
-
-
-(** The example in the Reference Manual *)
-
-Require Import ZArith.
-
-SearchAbout Z.mul Z.add "distr".
-SearchAbout "+"%Z "*"%Z "distr" -positive -Prop.
-SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas.