X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fhelp%2FC%2Fsec_tactics.xml;h=e03dece5bc1bd8ea612d0b4fdfe4153b66d9d899;hb=ccf5bef29f42897a28ee7cc797c3d5698adfcb1d;hp=193a0e3310f489c1c587955cc1a3210deed2f4a3;hpb=72dae1a44bbed06ff9daeadf53671e109a1b882f;p=helm.git

diff --git a/matita/help/C/sec_tactics.xml b/matita/help/C/sec_tactics.xml
index 193a0e331..e03dece5b 100644
--- a/matita/help/C/sec_tactics.xml
+++ b/matita/help/C/sec_tactics.xml
@@ -519,10 +519,10 @@
           <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