Documentation fixed.

diff --git a/helm/software/matita/help/C/sec_gettingstarted.xml b/helm/software/matita/help/C/sec_gettingstarted.xml
index f7d435e70733439a4230046d57cee1ae42fe256f..c1feb6d9249d142030b4238c3ae2e7a045450344 100644 (file)
--- a/helm/software/matita/help/C/sec_gettingstarted.xml
+++ b/helm/software/matita/help/C/sec_gettingstarted.xml
@@ -26,8 +26,7 @@
      </listitem>
      <listitem>Typing one of the following ligatures (and opzionally converting
       the ligature to the Unicode character has described before):
-      &quot;:=&quot; (which stands for ≝); &quot;->&quot; (which stands for &quot;→&quot;);
-      &quot;->&quot; (which stands for &quot;⇒&quot;).
+      &quot;:=&quot; (which stands for ≝); &quot;->&quot; (which stands for &quot;→&quot;); &quot;=>&quot; (which stands for &quot;⇒&quot;).
      </listitem>
     </itemizedlist>
   </sect1>

diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml
index 45459572bfc20affb08754727e141ba99d7f8474..dd2af7f5fe09596c922865c7f25e456cefb29de2 100644 (file)
--- a/helm/software/matita/help/C/sec_terms.xml
+++ b/helm/software/matita/help/C/sec_terms.xml
@@ -158,8 +158,8 @@
       <entry/>
       <entry>|</entry>
       <entry>&id;[<emphasis role="bold">\subst[</emphasis>
-       &id;<emphasis role="bold">â\89\9d</emphasis>&term;
-       [<emphasis role="bold">;</emphasis>&id;<emphasis role="bold">â\89\9d</emphasis>&term;]…
+       &id;<emphasis role="bold">â\89\94</emphasis>&term;
+       [<emphasis role="bold">;</emphasis>&id;<emphasis role="bold">â\89\94</emphasis>&term;]…
        <emphasis role="bold">]</emphasis>]
       </entry>
       <entry>identifier with optional explicit named substitution</entry>
@@ -249,16 +249,30 @@
       <entry id="args">&args;</entry>
       <entry>::=</entry>
       <entry>
-       [<emphasis role="bold">(</emphasis>]<emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;][<emphasis role="bold">)</emphasis>]
+       <emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;]
       </entry>
       <entry>ignored argument</entry>
      </row>
      <row>
       <entry/>
       <entry>|</entry>
-      <entry>[<emphasis role="bold">(</emphasis>]&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;][<emphasis role="bold">)</emphasis>]</entry>
+      <entry>
+       <emphasis role="bold">(</emphasis><emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis>
+      </entry>
+      <entry>ignored argument</entry>
+     </row>
+     <row>
+      <entry/>
+      <entry>|</entry>
+      <entry>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]</entry>
       <entry></entry>
      </row>
+     <row>
+      <entry/>
+      <entry>|</entry>
+      <entry><emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis></entry>
+      <entry/>
+     </row>
     </tbody>
    </tgroup>
   </table>