X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=caa069a0d839697cdbfc36e8a0c155bccfed1b3c;hb=aff007d80f87128884c96a664bc88aec69107d85;hp=0d06da71d0d7358dd863c68c210125a63fe2f252;hpb=05b509909ee5b61dbfca46d1239d64556af5ba2e;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 0d06da71d..caa069a0d 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -434,7 +434,14 @@ let letin_tac ~where ~what:(_,_,w) name =
  ]
 ;;
 
-let apply_tac (s,n,t) = exact_tac (s,n,Ast.Appl [t; Ast.Implicit `Vector]);;
+let apply_tac (s,n,t) = 
+  let t = 
+    match t with
+    | Ast.AttributedTerm (_,Ast.Binder _) | Ast.Binder _ -> t
+    | _ -> Ast.Appl [t; Ast.Implicit `Vector]
+  in
+    exact_tac (s,n,t)
+;;
 
 type indtyinfo = {
         rightno: int;
@@ -468,6 +475,7 @@ let elim_tac ~what:(txt,len,what) ~where =
   let compute_goal_sort_tac = distribute_tac (fun status goal ->
     let goalty = get_goalty status goal in
     let status, goalsort = typeof status (ctx_of goalty) goalty in
+    let goalsort = fix_sorts goalsort in
     sort := Some goalsort;
     exec id_tac status goal)
   in
@@ -514,7 +522,9 @@ let rewrite_tac ~dir ~what:(_,_,what) ~where status =
    | _ -> assert false 
  in
  let name =
-  match dir with `LeftToRight -> "eq_elim_r" | `RightToLeft -> "eq" ^ suffix
+  match dir with
+     `LeftToRight -> "eq" ^ suffix ^ "_r"
+   | `RightToLeft -> "eq" ^ suffix
  in
   block_tac
    [ select_tac ~where ~job:(`Substexpand 1) true;