aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Lists/Streams.v
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-04-13 17:10:32 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-04-13 17:10:32 +0000
commitfa348d2de6c479a2dd3722f9fdaf449e4e4345f1 (patch)
tree71a1c7a21c02fb430787b8d0517ed7912daf560e /theories/Lists/Streams.v
parent9737b8301b771832e250298e165801f695760551 (diff)
Correction bug #1499
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9767 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Lists/Streams.v')
-rw-r--r--theories/Lists/Streams.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
index 366172381..a8b55fb3e 100644
--- a/theories/Lists/Streams.v
+++ b/theories/Lists/Streams.v
@@ -14,9 +14,9 @@ Set Implicit Arguments.
Section Streams.
-Variable A : Set.
+Variable A : Type.
-CoInductive Stream : Set :=
+CoInductive Stream : Type :=
Cons : A -> Stream -> Stream.