X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_tactics.xml;h=e03dece5bc1bd8ea612d0b4fdfe4153b66d9d899;hb=06a19bec47845ecffe3bf9d9a95d3d4dadf76861;hp=193a0e3310f489c1c587955cc1a3210deed2f4a3;hpb=00e0c1d5cff8d5b5588185e1a70352a2e7a1a8e9;p=helm.git
diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index 193a0e331..e03dece5b 100644
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -519,10 +519,10 @@
Action:
- For each each premise H
- of type T in the current context
- where T is a non-recursive inductive type
- of sort Prop without right parameters, the tactic runs
+ For each each premise H of type
+ T in the current context where
+ T is a non-recursive inductive type without
+ right parameters and of sort Prop or CProp, the tactic runs
elim H as H1 ... Hm
, clears H and runs itself