diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-29 14:21:25 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-29 16:19:35 +0100 |
| commit | 654b69cbeb55a0cab3c2328d73355ad2510d1a85 (patch) | |
| tree | bcd94265271f4de9ccb9b0cefedd1bc2ee43eb9a /test-suite/bugs/closed/3267.v | |
| parent | dd1998f1a9bc2aae2e83aa4e349318d2466b6aea (diff) | |
Fixing another instance of bug #3267 in eauto, this time in the
presence of hints modifying the context and of a "using" clause.
Incidentally opening Hints by default in debugger.
Diffstat (limited to 'test-suite/bugs/closed/3267.v')
| -rw-r--r-- | test-suite/bugs/closed/3267.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3267.v b/test-suite/bugs/closed/3267.v index 5ce1ddf0c..8175d66ac 100644 --- a/test-suite/bugs/closed/3267.v +++ b/test-suite/bugs/closed/3267.v @@ -34,3 +34,14 @@ Module d. debug eauto. Defined. End d. + +(* An other variant which was still failing in 8.5 beta2 *) + +Parameter A B : Prop. +Axiom a:B. + +Hint Extern 1 => match goal with H:_ -> id _ |- _ => try (unfold id in H) end. +Goal (B -> id A) -> A. +intros. +eauto using a. +Abort. |