Demodulate used to be a reduction_kind and it used to take a ~pattern.

[helm.git] / helm / software / matita / help / C / sec_terms.xml

diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml
index d521ac87060a6a2e0a462fd8ae079e2235184696..945a43837bcfb79db57081fbb359579a1ec12be3 100644 (file)
--- a/helm/software/matita/help/C/sec_terms.xml
+++ b/helm/software/matita/help/C/sec_terms.xml
@@ -643,11 +643,6 @@
        <row>
        <entry id="grammar.reduction-kind">&reduction-kind;</entry>
        <entry>::=</entry>
-        <entry><emphasis role="bold">demodulate</emphasis></entry>
-       </row>
-       <row>
-        <entry/>
-        <entry>|</entry>
         <entry><emphasis role="bold">normalize</emphasis></entry>
         <entry>Computes the βδιζ-normal form</entry>
        </row>