First tests.

[helm.git] / helm / software / components / ng_tactics / nTactics.ml

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 67568154088e1d54f47c7b6de7662044166354ce..f6d8bfaec3055f456c70615207ed3fc74f98aa8b 100644 (file)
--- 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@