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 _ -> ())
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 ->