From ba6ec642e2554f5789bef601cb23209b7e93ab5c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 10 Nov 2006 18:37:26 +0000
Subject: Ajout de dépliage de l'énoncé, si besoin est, dans apply in

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9363 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/apply.v | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 4f26069633..30fa4129d7 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -12,3 +12,11 @@ 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.
+
+(* Check if it unfolds when there are not enough premises *)
+
+Goal forall n, n = S n -> False.
+intro.
+apply n_Sn in H.
+assumption.
+Qed.
-- 
cgit v1.2.3