diff --git a/theories/ereal.v b/theories/ereal.v
index 41a4dccd7..cc7447a54 100644
--- a/theories/ereal.v
+++ b/theories/ereal.v
@@ -14,7 +14,8 @@ Require Export constructive_ereal.
 (******************************************************************************)
 (*                   Extended real numbers, classical part                    *)
 (*                                                                            *)
-(* This is an addition to the file ereal.v with classical logic elements.     *)
+(* This is an addition to the file constructive_ereal.v with classical logic  *)
+(* elements.                                                                  *)
 (*                                                                            *)
 (*  (\sum_(i \in A) f i)%E == finitely supported sum, see fsbigop.v           *)
 (*                                                                            *)