diff options
Diffstat (limited to 'test-suite/success/apply.v')
| -rw-r--r-- | test-suite/success/apply.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 48db9c41c..7f1a8f5d4 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -489,3 +489,10 @@ split. exact H. (* Check that generated names are H and H0 *) exact H0. Qed. + +(* This failed at some time in between 18 August 2014 and 2 September 2014 *) + +Goal forall A B C: Prop, (True -> A -> B /\ C) -> A -> B. +intros * H. +apply H. +Abort. |