X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=b2a48c6fdcb9b1781b936ba12a9d947266d0079a;hb=efa63a8a299d6daf9e11820b03ab423eddd405f2;hp=16602ac9f6202276e623c7e206df3289c03c79a9;hpb=a425ea9290454065cf33d33f0ae13a1006fef5fd;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 16602ac9f..b2a48c6fd 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -303,7 +303,7 @@ let clear_tac names =
 
 let generalize0_tac args =
  if args = [] then id_tac
- else exact_tac ("",0,Ast.Appl (Ast.Implicit :: args))
+ else exact_tac ("",0,Ast.Appl (Ast.Implicit `JustOne :: args))
 ;;
 
 let select0_tac ~where:(wanted,hyps,where) ~job  =
@@ -429,11 +429,12 @@ let change_tac ~where ~with_what =
 let letin_tac ~where ~what:(_,_,w) name =
  block_tac [
   select_tac ~where ~job:(`Substexpand 1) true;
-  exact_tac ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit));
+  exact_tac
+   ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit `JustOne));
  ]
 ;;
 
-let apply_tac = exact_tac;;
+let apply_tac (s,n,t) = exact_tac (s,n,Ast.Appl [t; Ast.Implicit `Vector]);;
 
 type indtyinfo = {
         rightno: int;
@@ -450,7 +451,7 @@ let analyze_indty_tac ~what indtyref = distribute_tac (fun status goal ->
   let status, what = disambiguate status what None (ctx_of goalty) in
   let status, ty_what = typeof status (ctx_of what) what in 
   let status, (r,consno,lefts,rights) = analyse_indty status ty_what in
-  let leftno = List.length rights in
+  let leftno = List.length lefts in
   let rightno = List.length rights in
   indtyref := Some { 
     rightno = rightno; leftno = leftno; consno = consno;
@@ -486,7 +487,8 @@ let elim_tac ~what ~where =
        | _ -> assert false 
      in
      let holes = 
-       HExtlib.mk_list Ast.Implicit (ity.leftno+1+ ity.consno + ity.rightno) in
+      HExtlib.mk_list (Ast.Implicit `JustOne)
+       (ity.leftno+1+ ity.consno + ity.rightno) in
      let eliminator = 
        let _,_,w = what in
        Ast.Appl(Ast.Ident(name,None)::holes @ [ w ])
@@ -519,7 +521,7 @@ let rewrite_tac ~dir ~what:(_,_,what) ~where status =
    [ select_tac ~where ~job:(`Substexpand 1) true;
      exact_tac
       ("",0,
-       Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list Ast.Implicit 5 @
+       Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list (Ast.Implicit `JustOne) 5@
         [what]))] status
 ;;
 
@@ -527,7 +529,7 @@ let intro_tac name =
  block_tac
   [ exact_tac
      ("",0,(Ast.Binder (`Lambda,
-      (Ast.Ident (name,None),None),Ast.Implicit)));
+      (Ast.Ident (name,None),None),Ast.Implicit `JustOne)));
     if name = "_" then clear_tac [name] else id_tac ]
 ;;