\ldots are now used in nelim and ncases

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index b2a48c6fdcb9b1781b936ba12a9d947266d0079a..0d06da71d0d7358dd863c68c210125a63fe2f252 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -446,7 +446,8 @@ type indtyinfo = {
  }
 ;;
 
-let analyze_indty_tac ~what indtyref = distribute_tac (fun status goal ->
+let analyze_indty_tac ~what indtyref =
+ distribute_tac (fun status goal ->
   let goalty = get_goalty status goal in
   let status, what = disambiguate status what None (ctx_of goalty) in
   let status, ty_what = typeof status (ctx_of what) what in 
@@ -460,7 +461,8 @@ let analyze_indty_tac ~what indtyref = distribute_tac (fun status goal ->
   exec id_tac status goal)
 ;;
 
-let elim_tac ~what ~where = 
+let elim_tac ~what:(txt,len,what) ~where = 
+  let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in
   let indtyinfo = ref None in
   let sort = ref None in
   let compute_goal_sort_tac = distribute_tac (fun status goal ->
@@ -486,12 +488,9 @@ let elim_tac ~what ~where =
           "_rect_" ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] sort
        | _ -> assert false 
      in
-     let holes = 
-      HExtlib.mk_list (Ast.Implicit `JustOne)
-       (ity.leftno+1+ ity.consno + ity.rightno) in
      let eliminator = 
        let _,_,w = what in
-       Ast.Appl(Ast.Ident(name,None)::holes @ [ w ])
+       Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
      in
      exact_tac ("",0,eliminator) status) ]) 
 ;;
@@ -548,7 +547,8 @@ let cases ~what status goal =
  instantiate status goal t
 ;;
 
-let cases_tac ~what ~where = 
+let cases_tac ~what:(txt,len,what) ~where = 
+  let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in
   let indtyinfo = ref None in
   atomic_tac 
    (block_tac [