Fix test-suite files relying on tcs bugs

- One was expecting shelved goals to remain after resolution (from refine).
- The other too were relying on the wrong classification of subgoals
  as typeclass subgoals at toplevel.

1 files changed, 1 insertions, 1 deletions

diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
index f97f764b4d..3178c6fc15 100644
--- a/test-suite/success/bteauto.v
+++ b/test-suite/success/bteauto.v
@@ -1,3 +1,4 @@
+Require Import Program.Tactics.
 Module Backtracking.
   Class A := { foo : nat }.
 
@@ -8,7 +9,6 @@ Module Backtracking.
   Qed.
   
   Arguments foo A : clear implicits.
-  Require Import Program.Tactics.
   Example find42 : exists n, n = 42.
   Proof.
     eexists.