diff options
author | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
commit | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch) | |
tree | ad89c6bb57ceee608fcba2bb3435b74e0f57919e /test-suite/success/LetIn.v | |
parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) |
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'test-suite/success/LetIn.v')
-rw-r--r-- | test-suite/success/LetIn.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/test-suite/success/LetIn.v b/test-suite/success/LetIn.v index 0e0b4435..b61ea784 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. |