From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 31 Jul 2009 09:02:31 +0000 (+0000)
Subject: \ldots are now used in nelim and ncases
X-Git-Tag: make_still_working~3586
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=05b509909ee5b61dbfca46d1239d64556af5ba2e;p=helm.git

\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 b2a48c6fd..0d06da71d 100644
--- 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 [