Backporting the legacy Coq Stream library.

Makefile

@@ -55,7 +55,7 @@ FLOCQ=\
 
 # General-purpose libraries (in lib/)
 
-VLIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \
+VLIB=Axioms.v Coqlib.v Streams.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \
   Iteration.v Integers.v Archi.v Fappli_IEEE_extra.v Floats.v \
   Parmov.v UnionFind.v Wfsimpl.v \
   Postorder.v FSetAVLplus.v IntvSets.v Decidableplus.v BoolEqual.v

lib/Streams.v

@@ -0,0 +1,31 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+Set Implicit Arguments.
+
+CoInductive Stream (A : Type) : Type :=
+    Cons : A -> Stream A -> Stream A.
+
+Definition hd (A : Type) (x:Stream A) := match x with
+                            | Cons a _ => a
+                            end.
+
+Definition tl (A : Type) (x:Stream A) := match x with
+                            | Cons _ s => s
+                            end.
+
+CoFixpoint const (A : Type) (a : A) : Stream A := Cons a (const a).
+
+Unset Implicit Arguments.