]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/help/C/sec_tactics.xml
decompose: delta-expansion of the type to eliminate now works fine
[helm.git] / matita / help / C / sec_tactics.xml
index 193a0e3310f489c1c587955cc1a3210deed2f4a3..e03dece5bc1bd8ea612d0b4fdfe4153b66d9d899 100644 (file)
           <term>Action:</term>
           <listitem>
             <para>
-            For each each premise <command>H</command> 
-            of type <command>T</command> in the current context
-            where <command>T</command> is a non-recursive inductive type
-            of sort Prop without right parameters, the tactic runs
+            For each each premise <command>H</command> of type 
+            <command>T</command> in the current context where
+            <command>T</command> is a non-recursive inductive type without
+            right parameters and of sort Prop or CProp, the tactic runs
             <command> 
              elim H as H<subscript>1</subscript> ... H<subscript>m</subscript>
             </command>, clears <command>H</command>  and runs itself