X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=f6d8bfaec3055f456c70615207ed3fc74f98aa8b;hb=2589e631ad9c04a89cb7730d6bca913aed016f98;hp=67568154088e1d54f47c7b6de7662044166354ce;hpb=d272210a331d720b08d50b845fa21fa7ec0d4252;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 675681540..f6d8bfaec 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -22,7 +22,7 @@ module Ast = CicNotationPt
 
 let id_tac status = status ;;
 let print_tac print_status message status = 
-  if print_status then pp_status status;
+  if print_status then pp_tac_status status;
   prerr_endline message; 
   status
 ;;
@@ -541,7 +541,7 @@ let rewrite_tac ~dir ~what:(_,_,what) ~where status =
    | `RightToLeft -> "eq" ^ suffix
  in
   block_tac
-   [ select_tac ~where ~job:(`Substexpand 1) true;
+   [ select_tac ~where ~job:(`Substexpand 2) true;
      exact_tac
       ("",0,
        Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list (Ast.Implicit `JustOne) 5@