4 files changed, 77 insertions, 60 deletions
diff --git a/test-suite/success/ConversionOrder.v b/test-suite/success/ConversionOrder.v
new file mode 100644
index 0000000000..1e0b4dbf23
--- /dev/null
+++ b/test-suite/success/ConversionOrder.v
@@ -0,0 +1,16 @@
+(* The kernel may convert application arguments right to left,
+   resulting in ill-typed terms, but should be robust to them. *)
+
+Inductive Hide := hide : forall A, A -> Hide.
+
+Lemma foo : (hide Type Type) = (hide (nat -> Type) (fun x : nat => Type)).
+Proof.
+  Fail reflexivity.
+  match goal with |- ?l = _ => exact_no_check (eq_refl l) end.
+  Fail Defined.
+Abort.
+
+Definition HideMore (_:Hide) := 0.
+
+Definition foo : HideMore (hide Type Type) = HideMore (hide (nat -> Type) (fun x : nat => Type))
+  := eq_refl.
diff --git a/test-suite/success/InductiveVsImplicitsVsTC.v b/test-suite/success/InductiveVsImplicitsVsTC.v
new file mode 100644
index 0000000000..a98de32b70
--- /dev/null
+++ b/test-suite/success/InductiveVsImplicitsVsTC.v
@@ -0,0 +1,26 @@
+Module NoConv.
+  Class C := {}.
+
+  Definition useC {c:C} := nat.
+
+  Inductive foo {a b : C} := CC : useC -> foo.
+  (* If TC search runs before parameter unification it will pick the
+     wrong instance for the first parameter.
+
+     useC makes sure we don't completely skip TC search.
+   *)
+End NoConv.
+
+Module ForConv.
+
+  Class Bla := { bla : Type }.
+
+  Instance bli : Bla := { bla := nat }.
+
+  Inductive vs := C : forall x : bla, x = 2 -> vs.
+  (* here we need to resolve TC to pass the conversion problem if we
+     combined with the previous example it would fail as TC resolution
+     for conversion is unrestricted and so would resolve the
+     conclusion too early. *)
+
+End ForConv.
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.