fixes #853 (#854)

math-comp · Mar 24, 2023 · 7ea530f · 7ea530f
1 parent 30ad54d
commit 7ea530f
Showing 1 changed file with 2 additions and 1 deletion.
diff --git 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           *)
 (*                                                                            *)