From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001
From: Samuel Mimram <samuel.mimram@ens-lyon.org>
Date: Wed, 28 Jul 2004 21:54:47 +0000
Subject: Imported Upstream version 8.0pl1

---
 test-suite/success/Abstract.v8 | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)
 create mode 100644 test-suite/success/Abstract.v8

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

diff --git a/test-suite/success/Abstract.v8 b/test-suite/success/Abstract.v8
new file mode 100644
index 00000000..21a985bc
--- /dev/null
+++ b/test-suite/success/Abstract.v8
@@ -0,0 +1,26 @@
+
+(* 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