fixes backported from the new kernel

[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 3cae2f84c1866ad13d858e14eb32953176c38c13..15793c63acb9e71b45b1d8065a64a05623f390ec 100644 (file)
--- a/helm/software/matita/help/C/sec_terms.xml
+++ b/helm/software/matita/help/C/sec_terms.xml
@@ -729,12 +729,28 @@
     <title>auto-params</title>
     <para>&TODO;</para>
     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
-      <title>reduction-kind</title>
+      <title>auto-params</title>
       <tgroup cols="4">
       <tbody>
        <row>
        <entry id="grammar.autoparams">&autoparams;</entry>
        <entry>::=</entry>
+        <entry>[&simpleautoparam;]…
+               [<emphasis role="bold">by</emphasis>
+                &term; [&term;]…]
+        </entry>
+        <entry>&TODO;</entry>
+       </row>
+      </tbody>
+     </tgroup>
+    </table>
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+      <title>simple-auto-param</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+       <entry id="grammar.simpleautoparam">&simpleautoparam;</entry>
+       <entry>::=</entry>
         <entry><emphasis role="bold">depth=&nat;</emphasis></entry>
         <entry>&TODO;</entry>
        </row>