- fwd concrete syntax fixed

- decompose, fwd, lapply documentation fixed

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 9e1dffdcd48c226207b7da9ffd718303eb3ad1c2..20d57ef9e5ab6cc63b92778d972fdf4f8a952bc5 100644 (file)
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -110,7 +110,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
        (lazy_term_pp term) (pp_tactic_pattern pattern)
   | FwdSimpl (_, hyp, idents) -> 
       sprintf "fwd %s%s" hyp 
-        (match idents with [] -> "" | idents -> " " ^ pp_idents idents)
+        (match idents with [] -> "" | idents -> " as " ^ pp_idents idents)
   | Generalize (_, pattern, ident) ->
      sprintf "generalize %s%s" (pp_tactic_pattern pattern)
       (match ident with None -> "" | Some id -> " as " ^ id)

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 535e396a9324703959145a1e97b662ce9fc287e8..ad081d6641d1c8bd34b20478701404f95bb5e8e0 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -178,7 +178,7 @@ EXTEND
          GrafiteAst.Fold (loc, kind, t, p)
     | IDENT "fourier" ->
         GrafiteAst.Fourier loc
-    | IDENT "fwd"; hyp = IDENT; idents = OPT ident_list0 ->
+    | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
         let idents = match idents with None -> [] | Some idents -> idents in
         GrafiteAst.FwdSimpl (loc, hyp, idents)
     | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->

diff --git a/matita/help/C/sec_tactics.xml b/matita/help/C/sec_tactics.xml
index c10d2bd337aabc49384f3c7984677369e751fce8..bc5095fae94061d264bf51662680b1da622db51f 100644 (file)
--- a/matita/help/C/sec_tactics.xml
+++ b/matita/help/C/sec_tactics.xml
@@ -389,7 +389,11 @@
         <varlistentry role="tactic.synopsis">
           <term>Synopsis:</term>
           <listitem>
-            <para><emphasis role="bold">decompose</emphasis> &id; [&id;]… &intros-spec;</para>
+            <para>
+            <emphasis role="bold">decompose</emphasis>
+            [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]
+            &id; &intros-spec;
+           </para>
           </listitem>
         </varlistentry>
         <varlistentry>
@@ -750,13 +754,13 @@ its constructor takes no arguments.</para>
   <sect1 id="tac_fwd">
     <title>fwd</title>
     <titleabbrev>fwd</titleabbrev>
-    <para><userinput>fwd H</userinput></para>
+    <para><userinput>fwd H as H<subscript>0</subscript> ... H<subscript>n</subscript></userinput></para>
     <para>
       <variablelist>
         <varlistentry role="tactic.synopsis">
           <term>Synopsis:</term>
           <listitem>
-            <para><emphasis role="bold">fwd</emphasis> &id; [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]</para>
+            <para><emphasis role="bold">fwd</emphasis> &id; [<emphasis role="bold">as</emphasis> &id; [&id;]…]</para>
           </listitem>
         </varlistentry>
         <varlistentry>
@@ -775,16 +779,23 @@ its constructor takes no arguments.</para>
             This tactic is under development.
              It simplifies the current context by removing
             <command>H</command> using the following methods:
-            forward application of a suitable simplification theorem (chosen
-             automatically) of which the type of <command>H</command> is a
-             premise, decomposition, rewriting. 
+            forward application (by <command>lapply</command>) of a suitable
+            simplification theorem, chosen automatically, of which the type
+            of <command>H</command> is a premise, 
+            decomposition (by <command>decompose</command>),
+            rewriting (by <command>rewrite</command>).
+            <command>H<subscript>0</subscript> ... H<subscript>n</subscript></command>
+            are passed to the tactics <command>fwd</command> invokes, as
+             names for the premise they introduce.
            </para>
           </listitem>
         </varlistentry>
         <varlistentry>
           <term>New sequents to prove:</term>
           <listitem>
-            <para>None.</para>
+            <para>
+            The ones opened by the tactics <command>fwd</command> invokes.
+           </para>
           </listitem>
         </varlistentry>
       </variablelist>
@@ -1043,19 +1054,39 @@ its constructor takes no arguments.</para>
         <varlistentry>
           <term>Pre-conditions:</term>
           <listitem>
-            <para>TODO.</para>
+            <para>
+            <command>t</command> must have at least <command>d</command>
+            independent premises and <command>n</command> must not be
+            greater than <command>d</command>.
+           </para>
           </listitem>
         </varlistentry>
         <varlistentry>
           <term>Action:</term>
           <listitem>
-            <para>TODO.</para>
+            <para>
+            It invokes <command>letin H ≝ (t ? ... ?)</command>
+            with enough <command>?</command>'s to reach the 
+            <command>d</command>-th independent premise of
+            <command>t</command>
+            (<command>d</command> is maximum if unspecified).       
+            Then it istantiates (by <command>apply</command>) with
+            t<subscript>1</subscript>, ..., t<subscript>n</subscript>
+            the <command>?</command>'s corresponding to the first 
+            <command>n</command> independent premises of
+            <command>t</command>.
+            Usually the other <command>?</command>'s preceding the 
+            <command>n</command>-th independent premise of
+            <command>t</command> are istantiated as a consequence.
+           </para>
           </listitem>
         </varlistentry>
         <varlistentry>
           <term>New sequents to prove:</term>
           <listitem>
-            <para>TODO.</para>
+            <para>
+            The ones opened by the tactics <command>lapply</command> invokes.
+           </para>
           </listitem>
         </varlistentry>
       </variablelist>

diff --git a/matita/help/C/tactic_quickref.xml b/matita/help/C/tactic_quickref.xml
index e1f7eb434e1c530e1bef0f22fc0a38e1356bd10a..6a735eee247779b3bb19494190ebb2c3e556b92c 100644 (file)
--- a/matita/help/C/tactic_quickref.xml
+++ b/matita/help/C/tactic_quickref.xml
@@ -38,7 +38,11 @@
     <para><link linkend="tac_cut"><emphasis role="bold">cut</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]</para>
   </listitem>
   <listitem>
-    <para><link linkend="tac_decompose"><emphasis role="bold">decompose</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis><link linkend="grammar.id">id</link></emphasis>]… <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis></para>
+    <para>
+            <link linkend="tac_decompose"><emphasis role="bold">decompose</emphasis></link>
+            [<emphasis role="bold">(</emphasis>[<emphasis><link linkend="grammar.id">id</link></emphasis>]…<emphasis role="bold">)</emphasis>]
+            <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis>
+           </para>
   </listitem>
   <listitem>
     <para><link linkend="tac_demodulation"><emphasis role="bold">demodulation</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
@@ -80,7 +84,7 @@
     </para>
   </listitem>
   <listitem>
-    <para><link linkend="tac_fwd"><emphasis role="bold">fwd</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis role="bold">(</emphasis>[<emphasis><link linkend="grammar.id">id</link></emphasis>]…<emphasis role="bold">)</emphasis>]</para>
+    <para><link linkend="tac_fwd"><emphasis role="bold">fwd</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis><link linkend="grammar.id">id</link></emphasis>]…]</para>
   </listitem>
   <listitem>
     <para><link linkend="tac_generalize"><emphasis role="bold">generalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]</para>