diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-04-16 22:52:30 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-04-16 22:52:30 +0200 |
| commit | 216c6c89d53e58eefff5ac8d47e1c5e04cdbf4b0 (patch) | |
| tree | 58962cb52aaa7d5758806986d6b390e9f8d89559 | |
| parent | 48995a3f33d1c966954839348c6b04d65178c2f4 (diff) | |
| parent | 56eb5bb876aaf60b8f1b77e949d449d24adc9e44 (diff) | |
Merge PR #7269: Protecting against a "deprecated cofix" warning.
| -rw-r--r-- | theories/Lists/Streams.v | 2 |
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. |