aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Lists/Streams.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Lists/Streams.v')
-rw-r--r--theories/Lists/Streams.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
index 310c651e8..8a01b8fb1 100644
--- a/theories/Lists/Streams.v
+++ b/theories/Lists/Streams.v
@@ -196,7 +196,7 @@ Lemma ForAll_map : forall (P:Stream B -> Prop) (S:Stream A), ForAll (fun s => P
(map s)) S <-> ForAll P (map S).
Proof.
intros P S.
-split; generalize S; clear S; cofix; intros S; constructor;
+split; generalize S; clear S; cofix ForAll_map; intros S; constructor;
destruct H as [H0 H]; firstorder.
Qed.