From 070d631038dbf7ccbc8e0907c542588548ebe566 Mon Sep 17 00:00:00 2001
From: barras
Date: Wed, 24 Mar 2004 18:27:49 +0000
Subject: *** empty log message ***

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

diff --git a/test-suite/success/Abstract.v8 b/test-suite/success/Abstract.v8
new file mode 100644
index 0000000000..21a985bcde
--- /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