diff options
| author | Nick Lewycky | 2018-09-10 14:53:05 -0700 |
|---|---|---|
| committer | Nick Lewycky | 2018-09-19 18:13:23 -0700 |
| commit | a597bb33eb9b3c9d70422d72e89bcbda90896ddb (patch) | |
| tree | ce4983fd4b5a2e3c2a734c08cdf81e156c056f96 | |
| parent | df1f5bcd406a87c77601942f21d16555a8f6086e (diff) | |
Move tests in bugs/ to the bugs/closed/.
| -rw-r--r-- | test-suite/bugs/closed/2428.v (renamed from test-suite/bugs/2428.v) | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4623.v (renamed from test-suite/bugs/4623.v) | 0 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4624.v (renamed from test-suite/bugs/4624.v) | 0 | ||||
| -rw-r--r-- | test-suite/bugs/closed/7333.v (renamed from test-suite/bugs/7333.v) | 0 |
4 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/2428.v b/test-suite/bugs/closed/2428.v index a4f587a58d..b398a76d91 100644 --- a/test-suite/bugs/2428.v +++ b/test-suite/bugs/closed/2428.v @@ -5,6 +5,6 @@ Definition myFact := forall x, P x. Hint Extern 1 (P _) => progress (unfold myFact in *). Lemma test : (True -> myFact) -> P 3. -Proof. +Proof. intros. debug eauto. Qed. diff --git a/test-suite/bugs/4623.v b/test-suite/bugs/closed/4623.v index 7ecfd98b67..7ecfd98b67 100644 --- a/test-suite/bugs/4623.v +++ b/test-suite/bugs/closed/4623.v diff --git a/test-suite/bugs/4624.v b/test-suite/bugs/closed/4624.v index f5ce981cd0..f5ce981cd0 100644 --- a/test-suite/bugs/4624.v +++ b/test-suite/bugs/closed/4624.v diff --git a/test-suite/bugs/7333.v b/test-suite/bugs/closed/7333.v index fba5b9029d..fba5b9029d 100644 --- a/test-suite/bugs/7333.v +++ b/test-suite/bugs/closed/7333.v |