;;
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 = {