From bab2183aa03bd10917b2e1d915083ea8427f5d6c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 7 May 2014 08:31:51 +0200
Subject: Removing comment outdated since eta holds in conversion rule (this
 answers #3299).

---
 theories/Init/Logic.v | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index f994b4ca64..e944d3f041 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -229,10 +229,6 @@ Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3)
     is provided too.
 *)
 
-(** Remark: [exists x, Q] denotes [ex (fun x => Q)] so that [exists x,
-   P x] is in fact equivalent to [ex (fun x => P x)] which may be not
-   convertible to [ex P] if [P] is not itself an abstraction *)
-
 Inductive ex (A:Type) (P:A -> Prop) : Prop :=
   ex_intro : forall x:A, P x -> ex (A:=A) P.
 
-- 
cgit v1.2.3