diff options
| author | Théo Zimmermann | 2018-09-21 14:10:23 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-21 14:10:23 +0200 |
| commit | bceb3bc784d5ce196e06815bd91963607a35a62c (patch) | |
| tree | f4a18b7a40bddb054e373b3fbf287c77e246c9eb | |
| parent | 90ace7786901aa2f1253cf3887bf3e5221c5dae7 (diff) | |
| parent | a597bb33eb9b3c9d70422d72e89bcbda90896ddb (diff) | |
Merge PR #8455: Move tests in bugs/ to 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 |