The Coq mailing list

[Carlos.SIMPSON AT unice.fr]

Hello,
For what it's worth, I just unfolded out_eq within the proof engine 
which gave:
Definition p3:=
match ones as s return (ones = s :>Stream -> s = out s :>Stream) with
    | cons s => fun _ : ones = cons s :>Stream => refl_equal (out (cons s))
    end (refl_equal ones).

This typechecks to type (ones = cons ones).
Perhaps it is more of a problem in printing the result of ``Eval compute''.
(I don't claim to understand what all that means, though!)
---Carlos