some fixes here and there

[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 0030fd75abec375ef1cc06b0ab8d0da0c7206969..caa069a0d839697cdbfc36e8a0c155bccfed1b3c 100644 (file)
--- 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;