From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 18 Nov 2011 15:39:39 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~2085
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cffe307107c93392c8663ec246049c0e55d1ed69;p=helm.git

...
---

diff --git a/matita/matita/help/C/sec_commands.xml b/matita/matita/help/C/sec_commands.xml
index 3deaf4b51..a3a6cb8ed 100644
--- 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 4687868ad..2ac2cfc65 100644
--- 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>