the refiner was not checking that the resulting type

[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 caa069a0d839697cdbfc36e8a0c155bccfed1b3c..152c729d0d0f50ffdcc3d28c0f85c98aa1a32bd3 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -435,12 +435,8 @@ let letin_tac ~where ~what:(_,_,w) name =
 ;;
 
 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)
+  let t = Ast.Appl [t; Ast.Implicit `Vector] in
+  exact_tac (s,n,t)
 ;;
 
 type indtyinfo = {