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>☐</font> ==> HA \* HR + H1 \* ... \* HN \* <font size="-2">☐</font> ==> 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>☐</font>. + the last item of HR is always a <font size="-2">☐</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>☐</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">☐</font>. <div class="paragraph"> </div>