From 05b509909ee5b61dbfca46d1239d64556af5ba2e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 31 Jul 2009 09:02:31 +0000 Subject: [PATCH] \ldots are now used in nelim and ncases --- helm/software/components/ng_tactics/nTactics.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) 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 [ -- 2.39.2