1 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
new file mode 100644
index 00000000..4f260696
--- /dev/null
+++ b/test-suite/success/apply.v
@@ -0,0 +1,14 @@
+(* Test apply in *)
+
+Goal (forall x y, x = S y -> y=y) -> 2 = 4 -> 3=3.
+intros H H0.
+apply H in H0.
+assumption.
+Qed.
+
+Require Import ZArith.
+Open Scope Z_scope.
+Goal forall x y z, ~ z <= 0 -> x * z < y * z -> x <= y.
+intros; apply Znot_le_gt, Zgt_lt in H.
+apply Zmult_lt_reg_r, Zlt_le_weak in H0; auto.
+Qed.