From 4d4f08acb5e5f56d38289e5629173bc1b8b5fd57 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 21 Dec 2005 23:50:17 +0000
Subject: Abandon tests syntaxe v7; remplacement des .v par des fichiers en
 syntaxe v8

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

(limited to 'test-suite/success/Abstract.v')

diff --git a/test-suite/success/Abstract.v b/test-suite/success/Abstract.v
new file mode 100644
index 000000000..fc8800a56
--- /dev/null
+++ b/test-suite/success/Abstract.v
@@ -0,0 +1,27 @@
+
+(* Cf coqbugs #546 *)
+
+Require Import Omega.
+
+Section S.
+
+Variables n m : nat.
+Variable H : n<m.
+
+Inductive Dummy : nat -> Set :=
+| Dummy0 : Dummy 0
+| Dummy2 : Dummy 2
+| DummyApp : forall i j, Dummy i -> Dummy j -> Dummy (i+j).
+
+Definition Bug : Dummy (2*n).
+Proof.
+induction n.
+ simpl ; apply Dummy0.
+ replace (2 * S n0) with (2*n0 + 2) ; auto with arith.
+  apply DummyApp. 
+   2:exact Dummy2.
+   apply IHn0 ; abstract omega.
+Defined.
+
+End S.
+
-- 
cgit v1.2.3