cfml

diff --git a/Coq/CFML/CFHeaps.theory.xml b/Coq/CFML/CFHeaps.theory.xml
index c972d04..edccc68 100644
--- a/Coq/CFML/CFHeaps.theory.xml
+++ b/Coq/CFML/CFHeaps.theory.xml
@@ -484,10 +484,10 @@ Hints  <ht:DEFINITION uri="cic:/CFML/CFHeaps/Hsimpl_hint.ind" as="Inductive" lin
 Tactics 
 <br/>
 Maintain the goal in the form
-     H1 \* ... \* HN \* <font size=-2>&#9744;</font> ==&gt; HA \* HR
+     H1 \* ... \* HN \* <font size="-2">&#9744;</font> ==&gt; HA \* HR
    where HA is initially empty and accumulates elements not simplifiable
    and HR contains the values that are to be cancelled out;
-   the last item of HR is always a <font size=-2>&#9744;</font>.
+   the last item of HR is always a <font size="-2">&#9744;</font>.
    As long as HR is of the form H \* H', we try to match H with one of the Hi.
   <span class="inlinecode"><span class="id" title="var">hsimpls</span></span> is the same as <span class="inlinecode"><span class="id" title="var">hsimpl</span>;</span> <span class="inlinecode"><span class="id" title="tactic">subst</span></span>  <span class="inlinecode"><span class="id" title="var">hsimpl_credits</span></span> is the same as <span class="inlinecode"><span class="id" title="var">hsimpl</span></span> excepts that it tries
     to perform arithmetic to simplify credits. Note: to execute
diff --git a/Coq/CFML/CFTactics.theory.xml b/Coq/CFML/CFTactics.theory.xml
index cc162a2..edda3d4 100644
--- a/Coq/CFML/CFTactics.theory.xml
+++ b/Coq/CFML/CFTactics.theory.xml
@@ -1699,7 +1699,7 @@ Tactic Notation "xlets" constr(Q) :=
 
 <br/>
 Tactic <span class="inlinecode"><span class="id" title="var">xskip_credits</span></span> eliminates all occurrences of credits
-    in the goal, by replacing <span class="inlinecode">\$</span> <span class="inlinecode"><span class="id" title="var">x</span></span> with the empty heap predicate \<font size=-2>&#9744;</font>.
+    in the goal, by replacing <span class="inlinecode">\$</span> <span class="inlinecode"><span class="id" title="var">x</span></span> with the empty heap predicate \<font size="-2">&#9744;</font>.
 
 <div class="paragraph"> </div>