diff options
| author | Matthieu Sozeau | 2014-06-26 13:25:18 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-26 13:25:18 +0200 |
| commit | b443e5ce3ea09d82574b0a3196041737f0a5dcc7 (patch) | |
| tree | 0569f118991da38c6b9cbc45612415068e33ed0b /test-suite | |
| parent | 34570d23cf6ae7f6246b38e5094454b0eeea3e75 (diff) | |
Properly refresh the local hintdb database in case an external tactic changed
the hypotheses in eauto.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/3267.v (renamed from test-suite/bugs/opened/3267.v) | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/test-suite/bugs/opened/3267.v b/test-suite/bugs/closed/3267.v index 43eb1377d2..5ce1ddf0c4 100644 --- a/test-suite/bugs/opened/3267.v +++ b/test-suite/bugs/closed/3267.v @@ -1,16 +1,15 @@ Module a. - Hint Extern 0 => progress subst. + Local Hint Extern 0 => progress subst. Goal forall T (x y : T) (P Q : _ -> Prop), x = y -> (P x -> Q x) -> P y -> Q y. Proof. intros. (* this should not fail *) - Fail progress eauto. - admit. + progress eauto. Defined. End a. Module b. - Hint Extern 0 => progress subst. + Local Hint Extern 0 => progress subst. Goal forall T (x y : T) (P Q : _ -> Prop), y = x -> (P x -> Q x) -> P y -> Q y. Proof. intros. @@ -19,7 +18,7 @@ Module b. End b. Module c. - Hint Extern 0 => progress subst; eauto. + Local Hint Extern 0 => progress subst; eauto. Goal forall T (x y : T) (P Q : _ -> Prop), x = y -> (P x -> Q x) -> P y -> Q y. Proof. intros. @@ -28,10 +27,10 @@ Module c. End c. Module d. - Hint Extern 0 => progress subst; repeat match goal with H : _ |- _ => revert H end. + Local Hint Extern 0 => progress subst; repeat match goal with H : _ |- _ => revert H end. Goal forall T (x y : T) (P Q : _ -> Prop), x = y -> (P x -> Q x) -> P y -> Q y. Proof. intros. - eauto. + debug eauto. Defined. End d. |