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/Case12.v | 85 ++++++++++++++++++++++-----------------------
 1 file changed, 42 insertions(+), 43 deletions(-)

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

diff --git a/test-suite/success/Case12.v b/test-suite/success/Case12.v
index 284695f41..20073aa73 100644
--- a/test-suite/success/Case12.v
+++ b/test-suite/success/Case12.v
@@ -1,60 +1,59 @@
 (* This example was proposed by Cuihtlauac ALVARADO *)
 
-Require PolyList.
+Require Import List.
 
-Fixpoint mult2 [n:nat] : nat :=
-Cases n of
-| O => O
-| (S n) => (S (S (mult2 n)))
-end.
+Fixpoint mult2 (n : nat) : nat :=
+  match n with
+  | O => 0
+  | S n => S (S (mult2 n))
+  end.
 
 Inductive list : nat -> Set :=
-| nil : (list O)
-| cons : (n:nat)(list (mult2 n))->(list (S (S (mult2 n)))).
+  | nil : list 0
+  | cons : forall n : nat, list (mult2 n) -> list (S (S (mult2 n))).
 
 Type
-[P:((n:nat)(list n)->Prop);
- f:(P O nil);
- f0:((n:nat; l:(list (mult2 n)))
-      (P (mult2 n) l)->(P (S (S (mult2 n))) (cons n l)))]
- Fix F
-   {F [n:nat; l:(list n)] : (P n l) :=
-      <P>Cases l of
-        nil => f
-      | (cons n0 l0) => (f0 n0 l0 (F (mult2 n0) l0))
-      end}.
+  (fun (P : forall n : nat, list n -> Prop) (f : P 0 nil)
+     (f0 : forall (n : nat) (l : list (mult2 n)),
+           P (mult2 n) l -> P (S (S (mult2 n))) (cons n l)) =>
+   fix F (n : nat) (l : list n) {struct l} : P n l :=
+     match l as x0 in (list x) return (P x x0) with
+     | nil => f
+     | cons n0 l0 => f0 n0 l0 (F (mult2 n0) l0)
+     end).
 
 Inductive list' : nat -> Set :=
-| nil' : (list' O)
-| cons' : (n:nat)[m:=(mult2 n)](list' m)->(list' (S (S m))).
+  | nil' : list' 0
+  | cons' : forall n : nat, let m := mult2 n in list' m -> list' (S (S m)).
 
-Fixpoint length [n; l:(list' n)] : nat :=
-  Cases l of
-     nil' => O
-  | (cons' _ m l0) => (S (length m l0))
+Fixpoint length n (l : list' n) {struct l} : nat :=
+  match l with
+  | nil' => 0
+  | cons' _ m l0 => S (length m l0)
   end.
 
 Type
-[P:((n:nat)(list' n)->Prop);
- f:(P O nil');
- f0:((n:nat)
-      [m:=(mult2 n)](l:(list' m))(P m l)->(P (S (S m)) (cons' n l)))]
- Fix F
-   {F [n:nat; l:(list' n)] : (P n l) :=
-      <P>
-        Cases l of
-          nil' => f
-        | (cons' n0 m l0) => (f0 n0 l0 (F m l0))
-        end}.
+  (fun (P : forall n : nat, list' n -> Prop) (f : P 0 nil')
+     (f0 : forall n : nat,
+           let m := mult2 n in
+           forall l : list' m, P m l -> P (S (S m)) (cons' n l)) =>
+   fix F (n : nat) (l : list' n) {struct l} : P n l :=
+     match l as x0 in (list' x) return (P x x0) with
+     | nil' => f
+     | cons' n0 m l0 => f0 n0 l0 (F m l0)
+     end).
 
 (* Check on-the-fly insertion of let-in patterns for compatibility *)
 
 Inductive list'' : nat -> Set :=
-| nil'' : (list'' O)
-| cons'' : (n:nat)[m:=(mult2 n)](list'' m)->[p:=(S (S m))](list'' p).
-
-Check Fix length { length [n; l:(list'' n)] : nat :=
-         Cases l of
-           nil'' => O
-         | (cons'' n l0) => (S (length (mult2 n) l0))
-         end }.
+  | nil'' : list'' 0
+  | cons'' :
+      forall n : nat,
+      let m := mult2 n in list'' m -> let p := S (S m) in list'' p.
+
+Check
+  (fix length n (l : list'' n) {struct l} : nat :=
+     match l with
+     | nil'' => 0
+     | cons'' n l0 => S (length (mult2 n) l0)
+     end).
-- 
cgit v1.2.3