From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 26 May 2008 09:46:16 +0000 (+0000)
Subject: auto syntax updated
X-Git-Tag: make_still_working~5132
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f569c2d610c176b1d85de41968c2f3fbe2aef4e2;p=helm.git

auto syntax updated
---

diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index 764723261..812c8ed97 100644
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -184,7 +184,8 @@
         <varlistentry role="tactic.synopsis">
           <term>Synopsis:</term>
           <listitem>
-            <para><emphasis role="bold">auto</emphasis> &autoparams;</para>
+            <para><emphasis role="bold">auto</emphasis> &autoparams;. </para>
+            <para><emphasis role="bold">autobatch</emphasis> &autoparams;</para>
           </listitem>
         </varlistentry>
         <varlistentry>
@@ -195,7 +196,8 @@
              controlled by the optional <command>params</command>.
              Moreover, only lemmas whose type signature is a subset of the
              signature of the current sequent are considered. The signature of
-             a sequent is ...&TODO;</para>
+             a sequent is essentially the set of constats appearing in it.
+           </para>
           </listitem>
         </varlistentry>
         <varlistentry>
diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml
index 15793c63a..592e583e4 100644
--- a/helm/software/matita/help/C/sec_terms.xml
+++ b/helm/software/matita/help/C/sec_terms.xml
@@ -737,9 +737,8 @@
 	<entry>::=</entry>
         <entry>[&simpleautoparam;]…
                [<emphasis role="bold">by</emphasis>
-                &term; [&term;]…]
+                &term;, [&term;]…]
         </entry>
-        <entry>&TODO;</entry>
        </row>
       </tbody>
      </tgroup>
@@ -752,19 +751,34 @@
 	<entry id="grammar.simpleautoparam">&simpleautoparam;</entry>
 	<entry>::=</entry>
         <entry><emphasis role="bold">depth=&nat;</emphasis></entry>
-        <entry>&TODO;</entry>
+        <entry>Give a bound to the depth of the search tree</entry>
        </row>
        <row>
         <entry/>
         <entry>|</entry>
         <entry><emphasis role="bold">width=&nat;</emphasis></entry>
-        <entry>&TODO;</entry>
+        <entry>The maximal width of the search tree</entry>
        </row>
        <row>
         <entry/>
         <entry>|</entry>
-        <entry><emphasis role="bold">&TODO;</emphasis></entry>
-        <entry>&TODO;</entry>
+        <entry><emphasis role="bold">library</emphasis></entry>
+        <entry>Search everywhere (not only in included files)</entry>
+       </row>
+       <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><emphasis role="bold">type</emphasis></entry>
+        <entry>Try to close also goals of sort Type, otherwise only goals
+               living in sort Prop are attacked.
+        </entry>
+       </row>
+       <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><emphasis role="bold">paramodulation</emphasis></entry>
+        <entry>Try to close the goal performing unit-equality paramodulation
+        </entry>
        </row>
       </tbody>
      </tgroup>
diff --git a/helm/software/matita/help/C/tactics_quickref.xml b/helm/software/matita/help/C/tactics_quickref.xml
index 331d58dc2..a7c1ae3bd 100644
--- a/helm/software/matita/help/C/tactics_quickref.xml
+++ b/helm/software/matita/help/C/tactics_quickref.xml
@@ -29,7 +29,7 @@
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_auto"><emphasis role="bold">auto</emphasis></link> <emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis></entry>
+        <entry><link linkend="tac_auto"><emphasis role="bold">auto</emphasis></link> <emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis>. <emphasis role="bold">autobatch</emphasis> <emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis></entry>
       </row>
       <row>
         <entry/>