Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 9 insertions, 9 deletions

diff --git a/test-suite/success/Case1.v b/test-suite/success/Case1.v
index 2d5a5134..ea9b654d 100644
--- a/test-suite/success/Case1.v
+++ b/test-suite/success/Case1.v
@@ -2,14 +2,14 @@
 
 Section NATIND2.
 Variable P : nat -> Type.
-Variable H0 : (P O).
-Variable H1 : (P (S O)).
-Variable H2 : (n:nat)(P n)->(P (S (S n))).
-Fixpoint nat_ind2 [n:nat] : (P n) :=
-         <P>Cases n of  
-                        O     => H0
-                  | (S O)     => H1
-                  | (S (S n)) => (H2 n (nat_ind2 n))
-        end.
+Variable H0 : P 0.
+Variable H1 : P 1.
+Variable H2 : forall n : nat, P n -> P (S (S n)).
+Fixpoint nat_ind2 (n : nat) : P n :=
+  match n as x return (P x) with
+  | O => H0
+  | S O => H1
+  | S (S n) => H2 n (nat_ind2 n)
+  end.
 End NATIND2.