diff options
Diffstat (limited to 'test-suite/success/apply.v')
| -rw-r--r-- | test-suite/success/apply.v | 53 |
1 files changed, 53 insertions, 0 deletions
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index fcce68b9..952890ee 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -12,6 +12,44 @@ intros; apply Znot_le_gt, Zgt_lt in H. apply Zmult_lt_reg_r, Zlt_le_weak in H0; auto. Qed. +(* Test application under tuples *) + +Goal (forall x, x=0 <-> 0=x) -> 1=0 -> 0=1. +intros H H'. +apply H in H'. +exact H'. +Qed. + +(* Test as clause *) + +Goal (forall x, x=0 <-> (0=x /\ True)) -> 1=0 -> True. +intros H H'. +apply H in H' as (_,H'). +exact H'. +Qed. + +(* Test application modulo conversion *) + +Goal (forall x, id x = 0 -> 0 = x) -> 1 = id 0 -> 0 = 1. +intros H H'. +apply H in H'. +exact H'. +Qed. + +(* Check apply/eapply distinction in presence of open terms *) + +Parameter h : forall x y z : nat, x = z -> x = y. +Implicit Arguments h [[x] [y]]. +Goal 1 = 0 -> True. +intro H. +apply h in H || exact I. +Qed. + +Goal False -> 1 = 0. +intro H. +apply h || contradiction. +Qed. + (* Check if it unfolds when there are not enough premises *) Goal forall n, n = S n -> False. @@ -201,3 +239,18 @@ Axiom silly_axiom : forall v : exp, v = v -> False. Lemma silly_lemma : forall x : atom, False. intros x. apply silly_axiom with (v := x). (* fails *) + +(* Test non-regression of (temporary) bug 1981 *) + +Goal exists n : nat, True. +eapply ex_intro. +exact O. +trivial. +Qed. + +(* Test non-regression of (temporary) bug 1980 *) + +Goal True. +try eapply ex_intro. +trivial. +Qed. |