From 56eb5bb876aaf60b8f1b77e949d449d24adc9e44 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 16 Apr 2018 21:17:46 +0200 Subject: Protecting against a "deprecated cofix" warning. --- theories/Lists/Streams.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories') 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. -- cgit v1.2.3