X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnDestructTac.ml;h=8b2065a4393a1c3bcb12913a9fa106b40f161d27;hb=88efee4c688d660d2205c5933d302770acb5b407;hp=4f87707ebdc2f20c2ab33d0dd101788192daffd6;hpb=00da35cbf619e0d1f3d7fde7e6a0e6e4dc6c0915;p=helm.git

diff --git a/helm/software/components/ng_tactics/nDestructTac.ml b/helm/software/components/ng_tactics/nDestructTac.ml
index 4f87707eb..8b2065a43 100644
--- a/helm/software/components/ng_tactics/nDestructTac.ml
+++ b/helm/software/components/ng_tactics/nDestructTac.ml
@@ -206,7 +206,8 @@ let mk_discriminator it status =
                Some (CicNotationPt.Binder (`Lambda, (mk_id "y",None), 
                  CicNotationPt.Binder (`Forall, (mk_id "_", Some
                  (mk_appl [mk_id "eq";CicNotationPt.Implicit
-                 `JustOne;CicNotationPt.Implicit `JustOne;mk_id "y"])),
+                 `JustOne;(*CicNotationPt.Implicit `JustOne*)
+                  mk_appl (mk_id (kname it i)::ts);mk_id "y"])),
                  CicNotationPt.Implicit `JustOne ))),
                   List.map
                   (fun j ->