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

1 files changed, 8 insertions, 8 deletions

diff --git a/test-suite/success/LetIn.v b/test-suite/success/LetIn.v
index 0e0b44358..b61ea784b 100644
--- a/test-suite/success/LetIn.v
+++ b/test-suite/success/LetIn.v
@@ -1,11 +1,11 @@
 (* Simple let-in's *)
-Definition l1 := [P := O]P.
-Definition l2 := [P := nat]P.
-Definition l3 := [P := True]P.
-Definition l4 := [P := Prop]P.
-Definition l5 := [P := Type]P.
+Definition l1 := let P := 0 in P.
+Definition l2 := let P := nat in P.
+Definition l3 := let P := True in P.
+Definition l4 := let P := Prop in P.
+Definition l5 := let P := Type in P.
 
 (* Check casting of let-in *)
-Definition l6 := [P := O : nat]P.
-Definition l7 := [P := True : Prop]P.
-Definition l8 := [P := True : Type]P.
+Definition l6 := let P := 0:nat in P.
+Definition l7 := let P := True:Prop in P.
+Definition l8 := let P := True:Type in P.