diff options
| -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 |