X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=c45e825a40359ff75fbe464416d19d9bc692760c;hb=65e8f1ba961ef81c5604168e7f1c891063c1ec76;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..c45e825a4 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
 ;;
@@ -420,12 +420,12 @@ let generalize_tac ~where =
 ;;
 
 let cut_tac t = 
- block_tac [ 
+ atomic_tac (block_tac [ 
   exact_tac ("",0, Ast.Appl [Ast.Implicit `JustOne; Ast.Implicit `JustOne]);
   branch_tac;
    pos_tac [3]; exact_tac t;
    shift_tac; pos_tac [2]; skip_tac;
-  merge_tac ]
+  merge_tac ])
 ;;
 
 let lapply_tac (s,n,t) = 
@@ -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@
@@ -556,6 +556,25 @@ let intro_tac name =
     if name = "_" then clear_tac [name] else id_tac ]
 ;;
 
+let name_counter = ref 0;;
+let intros_tac ?names_ref names s =
+  let names_ref, prefix = 
+    match names_ref with | None -> ref [], "__" | Some r -> r, "H" 
+  in
+  if names = [] then
+   repeat_tac 
+     (fun s ->
+        incr name_counter;
+        (* TODO: generate better names *)
+        let name = prefix ^ string_of_int !name_counter in
+        let s = intro_tac name s in 
+        names_ref := !names_ref @ [name];
+        s)
+     s
+   else
+     block_tac (List.map intro_tac names) s
+;;
+
 let cases ~what status goal =
  let gty = get_goalty status goal in
  let status, what = disambiguate status (ctx_of gty) what None in