diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-10-29 12:37:46 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-11-03 16:26:40 +0100 |
| commit | d51c384e52003668bd97ca44da77a14c91e5cb14 (patch) | |
| tree | de591c962766ca0d826bec7620a35b41aa2730c7 /test-suite/success/bteauto.v | |
| parent | 0ab187ee578f0ef49ecf484278b8d3569630ee48 (diff) | |
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.
Diffstat (limited to 'test-suite/success/bteauto.v')
| -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 f97f764b4..3178c6fc1 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. |