...

diff --git a/matita/matita/help/C/sec_commands.xml b/matita/matita/help/C/sec_commands.xml
index 3deaf4b517ae381d6f1bfe0419f22de521c83278..a3a6cb8ed01d44b51dcc91da537809878acbf544 100644 (file)
--- a/matita/matita/help/C/sec_commands.xml
+++ b/matita/matita/help/C/sec_commands.xml
@@ -326,8 +326,36 @@
             hints (<link linkend="command_alias">aliases</link>).
             On the contrary, theorem and definitions declared in a file can be
            immediately used without including it.</para>
-          <para>The file <command>s</command> is automatically compiled
-         if it is not compiled yet.
+           <para>The file <command>s</command> is automatically compiled
+          if it is not compiled yet.
+          </para>
+          <para>
+          If the file <command>s</command> was already included, either
+          directly or recursively, the commands does nothing.
+          </para>
+         </listitem>
+       </varlistentry>
+     </variablelist>
+   </para>
+ </sect1>
+ <sect1 id="command_include_alias">
+   <title>include alias</title>
+   <para><userinput>include alias &quot;s&quot;</userinput></para>
+   <para>
+     <variablelist>
+       <varlistentry>
+         <term>Synopsis:</term>
+         <listitem>
+           <para><emphasis role="bold">include</emphasis> <emphasis role="bold">alias</emphasis> &qstring;</para>
+         </listitem>
+       </varlistentry>
+       <varlistentry>
+         <term>Action:</term>
+         <listitem>
+           <para>Every 
+            <link linkend="interpretation">interpretation</link>
+            declared in the file <command>s</command> is re-declared
+            so to make it the preferred choice for disambiguation.
           </para>
          </listitem>
        </varlistentry>

diff --git a/matita/matita/help/C/sec_tactics.xml b/matita/matita/help/C/sec_tactics.xml
index 4687868addfeb344ed8c7d46a190c58f31ddf192..2ac2cfc65a459961f869ccbb7644437f7c4c7e04 100644 (file)
--- a/matita/matita/help/C/sec_tactics.xml
+++ b/matita/matita/help/C/sec_tactics.xml
@@ -167,7 +167,7 @@
       </variablelist>
     </para>
   </sect1>
-  <sect1 id="tac_intro">
+  <sect1 id="macro_intro">
     <title>##</title>
     <titleabbrev>##</titleabbrev>
     <para><userinput>##</userinput></para>