Skip to content
Snippets Groups Projects
coquelicot 1.88 KiB
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: &Sigma; 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>  &#8746; {+ &infin;} &#8746; {- &infin;}  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>  &#8746; {+ infin} &#8746; {- 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)