napply now automatically inserts \ldots at the end

[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 445ac030e7674e758998ac74543a84162b05e991..b2a48c6fdcb9b1781b936ba12a9d947266d0079a 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -434,7 +434,7 @@ let letin_tac ~where ~what:(_,_,w) name =
  ]
 ;;
 
-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;