diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-05-07 08:31:51 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-05-07 08:31:51 +0200 |
| commit | bab2183aa03bd10917b2e1d915083ea8427f5d6c (patch) | |
| tree | 9389145ae11ad6cf4c93f07cf8c00a242ab01096 /theories/Init/Logic.v | |
| parent | 87e9c331253236b58048f0e9f5d4feea7b5fb04d (diff) | |
Removing comment outdated since eta holds in conversion rule (this
answers #3299).
Diffstat (limited to 'theories/Init/Logic.v')
| -rw-r--r-- | theories/Init/Logic.v | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index f994b4ca6..e944d3f04 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. |