X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_tactics%2FnDestructTac.ml;fp=matitaB%2Fcomponents%2Fng_tactics%2FnDestructTac.ml;h=d50a98f0880ba1ce09cbe32632fd3f64642f25b5;hb=86b0a224bd9251ed22648de04bc0d00f11dbd0fc;hp=dcd77499427218fa0487fbd504b8667325875132;hpb=e499c2e36d8a39c4749b8e0e34438b49532d15b8;p=helm.git

diff --git a/matitaB/components/ng_tactics/nDestructTac.ml b/matitaB/components/ng_tactics/nDestructTac.ml
index dcd774994..d50a98f08 100644
--- a/matitaB/components/ng_tactics/nDestructTac.ml
+++ b/matitaB/components/ng_tactics/nDestructTac.ml
@@ -28,7 +28,7 @@
 open NTacStatus
 open Continuationals.Stack
 
-let debug = false
+let debug = true
 let pp = 
   if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ())
 
@@ -638,13 +638,12 @@ let select_eq ctx acc domain status goal =
 
 let tagged_intro_tac curtag name =
   match curtag with
-  | _ -> NTactics.intro_tac name
-(*  | `Eq use_jmeq ->
+  | `Eq false ->
       NTactics.block_tac
         [ NTactics.intro_tac name 
         ; NTactics.reduce_tac 
-            ~reduction:(`Whd true) ~where:((if use_jmeq then hp_pattern_jm else
-                    hp_pattern) name) ] *)
+            ~reduction:(`Whd true) ~where:(hp_pattern name) ]
+  | _ -> NTactics.intro_tac name
         
 (*        status in
       distribute_tac (fun s g ->