fixes #853 (#854)

Author: affeldt-aist

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           *)
 (*                                                                            *)