(no commit message)

[helm.git] / matitaB / components / ng_tactics / nDestructTac.ml

diff --git a/matitaB/components/ng_tactics/nDestructTac.ml b/matitaB/components/ng_tactics/nDestructTac.ml
index dcd77499427218fa0487fbd504b8667325875132..d50a98f0880ba1ce09cbe32632fd3f64642f25b5 100644 (file)
--- 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 ->