From c01357249f005ee5ee531351c848e1410b970b6e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 13 Dec 2006 09:58:09 +0000
Subject: Dépliage du terme d'induction avant suppression quand celui-ci est un
 terme arbitraire, possiblement dépendant, qui a été transformé en let-in (cf
 success/destruct.v)

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

(limited to 'test-suite')

diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 9f938e10f4..ada292f186 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -23,3 +23,9 @@ set (b := true) in *.
 try destruct b.
 Abort.
 
+(* Used to fail with error "n is used in conclusion" before revision 9447 *)
+
+Goal forall n, n = S n.
+induction S.
+Abort.
+
-- 
cgit v1.2.3