Newer
Older
diff --git a/Coq/Coquelicot/PSeries.theory.xml b/Coq/Coquelicot/PSeries.theory.xml
index dea0fcb..31b023a 100644
--- a/Coq/Coquelicot/PSeries.theory.xml
+++ b/Coq/Coquelicot/PSeries.theory.xml
@@ -60,7 +60,7 @@ COPYING file for more details.
<ht:REQUIRE uri="cic:/Coquelicot/Derive"/>
<ht:REQUIRE uri="cic:/Coquelicot/Seq_fct"/>
<ht:REQUIRE uri="cic:/Coquelicot/Series"/>
- This file describes power series: Σ a<sub>k</sub>
+ This file describes power series: Sigma a<sub>k</sub>
x<sup>k</sup>. It contains definition, equivalence with the standard
library, differentiability, integrability, and many results about the
convergence circle. <ht:SECTION uri="cic:/Coquelicot/PSeries/Definitions" line="32">
diff --git a/Coq/Coquelicot/Rbar.theory.xml b/Coq/Coquelicot/Rbar.theory.xml
index c27518c..97cab72 100644
--- a/Coq/Coquelicot/Rbar.theory.xml
+++ b/Coq/Coquelicot/Rbar.theory.xml
@@ -49,7 +49,7 @@ COPYING file for more details.
<ht:REQUIRE uri="cic:/mathcomp/ssreflect/ssreflect"/>
<ht:REQUIRE uri="cic:/Coquelicot/Rcomplements"/>
This file contains the definition and properties of the set
- <span class="inlinecode"><span class="id" title="var">R</span></span> ∪ {+ ∞} ∪ {- ∞} denoted by <span class="inlinecode"><span class="id" title="var">Rbar</span></span>. We have defined:
+ <span class="inlinecode"><span class="id" title="var">R</span></span> ∪ {+ infin} ∪ {- infin} denoted by <span class="inlinecode"><span class="id" title="var">Rbar</span></span>. We have defined:
<ul class="doclist">
<li> coercions from <span class="inlinecode"><span class="id" title="var">R</span></span> to <span class="inlinecode"><span class="id" title="var">Rbar</span></span> and vice versa (<span class="inlinecode"><span class="id" title="var">Finite</span></span> gives <span class="inlinecode"><span class="id" title="var">R0</span></span> at infinity points)