diff options
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/bteauto.v | 2 |
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. |