bugfix ind docbook code for the relise of matita 0.99.3

diff --git a/matita/matita/help/C/sec_commands.xml b/matita/matita/help/C/sec_commands.xml
index 6c9ad43af74097f740569d63d827fbf3424fbd96..919f71451f63b99884f7037c2a14e240abb92126 100644 (file)
--- a/matita/matita/help/C/sec_commands.xml
+++ b/matita/matita/help/C/sec_commands.xml
@@ -352,8 +352,8 @@
             <link linkend="interpretation">interpretation</link> that was active
             when the file <command>s</command> was compiled last time
             is made active. The same happens for declarations of
-            <link linkend="command_default">default definitions and
-            theorems</link> and disambiguation
+            <!-- <link linkend="command_default">default definitions and
+            theorems</link> and --> disambiguation
             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>
@@ -534,7 +534,6 @@
        </varlistentry>
      </variablelist>
    </para>
-   -->
  </sect1>
  <sect1 id="command_universe_constraints">
    <title>universe constraint</title>

diff --git a/matita/matita/help/C/sec_tactics.xml b/matita/matita/help/C/sec_tactics.xml
index 2ac2cfc65a459961f869ccbb7644437f7c4c7e04..82802e2396b7ab95c08ba3b623bdee849be26c04 100644 (file)
--- a/matita/matita/help/C/sec_tactics.xml
+++ b/matita/matita/help/C/sec_tactics.xml
@@ -11,7 +11,7 @@
   </sect1>
 
   <sect1 id="tac_apply">
-    <title>@</title>
+    <title>apply</title>
     <titleabbrev>@</titleabbrev>
     <para><userinput>@t</userinput></para>
     <para>
@@ -52,7 +52,7 @@
     </para>
   </sect1>
   <sect1 id="tac_auto">
-    <title>//</title>
+    <title>auto</title>
     <titleabbrev>//</titleabbrev>
     <para><userinput>/params/</userinput></para>
     <para>
@@ -94,7 +94,7 @@
     </para>
   </sect1>
   <sect1 id="tac_intro">
-    <title>#</title>
+    <title>intro</title>
     <titleabbrev>#</titleabbrev>
     <para><userinput>#H</userinput></para>
     <para>
@@ -132,7 +132,7 @@
     </para>
   </sect1>
   <sect1 id="tac_intro_clear">
-    <title>#_</title>
+    <title>intro_clear</title>
     <titleabbrev>#_</titleabbrev>
     <para><userinput>#_</userinput></para>
     <para>
@@ -168,7 +168,7 @@
     </para>
   </sect1>
   <sect1 id="macro_intro">
-    <title>##</title>
+    <title>macro_input</title>
     <titleabbrev>##</titleabbrev>
     <para><userinput>##</userinput></para>
     <para>
@@ -198,7 +198,7 @@
     </para>
   </sect1>
   <sect1 id="tac_clear">
-    <title>-</title>
+    <title>clear</title>
     <titleabbrev>-</titleabbrev>
     <para><userinput>-H</userinput></para>
     <para>
@@ -239,7 +239,7 @@
     </para>
   </sect1>
   <sect1 id="tac_constructor">
-    <title>%</title>
+    <title>constructor</title>
     <titleabbrev>%</titleabbrev>
     <para><userinput>%n {args}</userinput></para>
     <para>
@@ -279,7 +279,7 @@
     </para>
   </sect1>
   <sect1 id="tac_decompose">
-    <title>*</title>
+    <title>decompose</title>
     <titleabbrev>*</titleabbrev>
     <para><userinput>
      * as H
@@ -326,7 +326,7 @@
     </para>
   </sect1>
   <sect1 id="tac_rewrite">
-    <title>></title>
+    <title>rewrite</title>
     <titleabbrev>></titleabbrev>
     <para><userinput>> p patt</userinput></para>
     <para>

diff --git a/matita/matita/help/C/sec_usernotation.xml b/matita/matita/help/C/sec_usernotation.xml
index e141bd85997a9a82ea23adf6395b2c9ab0867587..2972f8cb6455421cfca4c653e5926e30ce484245 100644 (file)
--- a/matita/matita/help/C/sec_usernotation.xml
+++ b/matita/matita/help/C/sec_usernotation.xml
@@ -2,7 +2,7 @@
 <!-- ============ User Notation ====================== -->
 <chapter id="sec_usernotation">
  <title>Extending the syntax</title>
-  Introduction: &TODO;
+<!--  Introduction: &TODO; -->
  <sect1>
   <title>notation</title>
   <titleabbrev>notation</titleabbrev>

diff --git a/matita/matita/help/C/tactics_quickref.xml b/matita/matita/help/C/tactics_quickref.xml
index 12e450fdf49da7e988b91a4790a25f50eb9e7043..6da96f66d1fc1852e577a381680d19f3a87d932d 100644 (file)
--- a/matita/matita/help/C/tactics_quickref.xml
+++ b/matita/matita/help/C/tactics_quickref.xml
@@ -5,115 +5,97 @@
       <row>
         <entry id="grammar.tactic">&tactic;</entry>
         <entry>::=</entry>
-        <entry>
-          <link linkend="tac_#">
-            <emphasis role="bold">#</emphasis>
-          </link>
-          <emphasis>
-            <link linkend="grammar.id">id</link>
-          </emphasis>
-        </entry>
+        <entry><emphasis role="bold">@</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry>
-          <link linkend="tac_##">
-            <emphasis role="bold">##</emphasis>
-          </link>
-        </entry>
+        <entry><link linkend="tac_applyS"><emphasis role="bold">applyS</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis></entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
         <entry>
-          <link linkend="tac_#_">
-            <emphasis role="bold">#_</emphasis>
+          <link linkend="tac_assumption">
+            <emphasis role="bold">assumption</emphasis>
           </link>
         </entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_%"><emphasis role="bold">%</emphasis></link> [<emphasis><link linkend="grammar.nat">nat</link></emphasis>] [<emphasis role="bol">{</emphasis><emphasis><link linkend="grammar.sterm">sterm</link></emphasis>…<emphasis role="bol">}</emphasis>]</entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry>
-            <link linkend="tac_*"><emphasis role="bold">*</emphasis></link>
-            [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]
-           </entry>
+        <entry><emphasis role="bold">/</emphasis><emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis><emphasis role="bold">/</emphasis>. </entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
         <entry>
-            <link linkend="tac_-"><emphasis role="bold">-</emphasis></link><emphasis><link linkend="grammar.id">id</link></emphasis>
+            <link linkend="tac_cases"><emphasis role="bold">cases</emphasis></link>
+            <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis>
            </entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><emphasis role="bold">/</emphasis><emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis><emphasis role="bold">/</emphasis>. </entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry>[<emphasis role="bold">&lt;</emphasis>|<link linkend="tac_&gt;"><emphasis role="bold">&gt;</emphasis></link>] <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
+        <entry><link linkend="tac_change"><emphasis role="bold">change</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> <emphasis role="bold">with</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_@"><emphasis role="bold">@</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
+        <entry>
+            <emphasis role="bold">-</emphasis><emphasis><link linkend="grammar.id">id</link></emphasis>
+           </entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_applyS"><emphasis role="bold">applyS</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis></entry>
+        <entry><emphasis role="bold">%</emphasis> [<emphasis><link linkend="grammar.nat">nat</link></emphasis>] [<emphasis role="bol">{</emphasis><emphasis><link linkend="grammar.sterm">sterm</link></emphasis>…<emphasis role="bol">}</emphasis>]</entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry>
-          <link linkend="tac_assumption">
-            <emphasis role="bold">assumption</emphasis>
-          </link>
-        </entry>
+        <entry><link linkend="tac_cut"><emphasis role="bold">cut</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
         <entry>
-            <link linkend="tac_cases"><emphasis role="bold">cases</emphasis></link>
-            <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis>
+            <emphasis role="bold">*</emphasis>
+            [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]
            </entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_change"><emphasis role="bold">change</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> <emphasis role="bold">with</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
+        <entry><link linkend="tac_destruct"><emphasis role="bold">destruct</emphasis></link>
+             [<emphasis role="bold">(</emphasis><emphasis><link linkend="grammar.id">id</link></emphasis>…<emphasis role="bold">)</emphasis>] [<emphasis role="bold">skip</emphasis> <emphasis role="bold">(</emphasis><emphasis><link linkend="grammar.id">id</link></emphasis>…<emphasis role="bold">)</emphasis>]</entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_cut"><emphasis role="bold">cut</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
+        <entry><link linkend="tac_elim"><emphasis role="bold">elim</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_destruct"><emphasis role="bold">destruct</emphasis></link>
-             [<emphasis role="bold">(</emphasis><emphasis><link linkend="grammar.id">id</link></emphasis>…<emphasis role="bold">)</emphasis>] [<emphasis role="bold">skip</emphasis> <emphasis role="bold">(</emphasis><emphasis><link linkend="grammar.id">id</link></emphasis>…<emphasis role="bold">)</emphasis>]</entry>
+        <entry><link linkend="tac_generalize"><emphasis role="bold">generalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_elim"><emphasis role="bold">elim</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
+        <entry>
+          <emphasis role="bold">#</emphasis>
+          <emphasis>
+            <link linkend="grammar.id">id</link>
+          </emphasis>
+        </entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_generalize"><emphasis role="bold">generalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
+        <entry>
+          <emphasis role="bold">#_</emphasis>
+        </entry>
       </row>
       <row>
         <entry/>
@@ -133,12 +115,24 @@
         <entry>|</entry>
         <entry><link linkend="tac_letin"><emphasis role="bold">letin</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold">≝</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
       </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry>
+          <emphasis role="bold">##</emphasis>
+        </entry>
+      </row>
       <row>
         <entry/>
         <entry>|</entry>
         <entry><link linkend="tac_normalize"><emphasis role="bold">normalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis>
              [<emphasis role="bold">nodelta</emphasis>]</entry>
       </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry>[<emphasis role="bold">&lt;</emphasis>|<emphasis role="bold">&gt;</emphasis>] <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
+      </row>
       <row>
         <entry/>
         <entry>|</entry>