X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=67568154088e1d54f47c7b6de7662044166354ce;hb=d272210a331d720b08d50b845fa21fa7ec0d4252;hp=4ce980b28e60ca2b14b77397ef9415713b62e7ff;hpb=42f25c258b0b199ee96dd8eaa3d44c86eb6916ab;p=helm.git diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 4ce980b28..675681540 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -13,37 +13,23 @@ open Printf -let debug = true +let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () -exception Error of string lazy_t -let fail msg = raise (Error msg) - -type lowtac_status = { - pstatus : NCic.obj; - lstatus : LexiconEngine.status -} - -type lowtactic = lowtac_status * int -> lowtac_status * int list * int list - -type tac_status = { - gstatus : Continuationals.Stack.t; - istatus : lowtac_status; -} - -type tactic = tac_status -> tac_status - -type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input +open Continuationals.Stack +open NTacStatus +module Ast = CicNotationPt -let pp_tac_status status = - prerr_endline (NCicPp.ppobj status.istatus.pstatus) +let id_tac status = status ;; +let print_tac print_status message status = + if print_status then pp_status status; + prerr_endline message; + status ;; -open Continuationals.Stack - let dot_tac status = - let new_gstatus = - match status.gstatus with + let gstatus = + match status#stack with | [] -> assert false | ([], _, [], _) :: _ as stack -> (* backward compatibility: do-nothing-dot *) @@ -57,25 +43,26 @@ let dot_tac status = (([ loc ], t, k, tag) :: s) | _ -> fail (lazy "can't use \".\" here") in - { status with gstatus = new_gstatus } + status#set_stack gstatus ;; -let branch_tac status = - let new_gstatus = - match status.gstatus with +let branch_tac ?(force=false) status = + let gstatus = + match status#stack with | [] -> assert false | (g, t, k, tag) :: s -> match init_pos g with (* TODO *) - | [] | [ _ ] -> fail (lazy "too few goals to branch"); + | [] -> fail (lazy "empty goals") + | [_] when (not force) -> fail (lazy "too few goals to branch") | loc :: loc_tl -> ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s in - { status with gstatus = new_gstatus } + status#set_stack gstatus ;; let shift_tac status = - let new_gstatus = - match status.gstatus with + let gstatus = + match status#stack with | (g, t, k, `BranchTag) :: (g', t', k', tag) :: s -> (match g' with | [] -> fail (lazy "no more goals to shift") @@ -84,12 +71,12 @@ let shift_tac status = :: (loc_tl, t', k', tag) :: s)) | _ -> fail (lazy "can't shift goals here") in - { status with gstatus = new_gstatus } + status#set_stack gstatus ;; let pos_tac i_s status = - let new_gstatus = - match status.gstatus with + let gstatus = + match status#stack with | [] -> assert false | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s when is_fresh loc -> @@ -98,35 +85,55 @@ let pos_tac i_s status = :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s) | _ -> fail (lazy "can't use relative positioning here") in - { status with gstatus = new_gstatus } + status#set_stack gstatus +;; + +let case_tac lab status = + let gstatus = + match status#stack with + | [] -> assert false + | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s + when is_fresh loc -> + let l_js = + List.filter + (fun curloc -> + let _,_,metasenv,_,_ = status#obj in + match NCicUtils.lookup_meta (goal_of_loc curloc) metasenv with + attrs,_,_ when List.mem (`Name lab) attrs -> true + | _ -> false) ([loc] @+ g') in + ((l_js, t , [],`BranchTag) + :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s) + | _ -> fail (lazy "can't use relative positioning here") + in + status#set_stack gstatus ;; let wildcard_tac status = - let new_gstatus = - match status.gstatus with + let gstatus = + match status#stack with | [] -> assert false | ([ loc ] , t, [], `BranchTag) :: (g', t', k', tag) :: s when is_fresh loc -> (([loc] @+ g', t, [], `BranchTag) :: ([], t', k', tag) :: s) | _ -> fail (lazy "can't use wildcard here") in - { status with gstatus = new_gstatus } + status#set_stack gstatus ;; let merge_tac status = - let new_gstatus = - match status.gstatus with + let gstatus = + match status#stack with | [] -> assert false | (g, t, k,`BranchTag) :: (g', t', k', tag) :: s -> ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s) | _ -> fail (lazy "can't merge goals here") in - { status with gstatus = new_gstatus } + status#set_stack gstatus ;; let focus_tac gs status = - let new_gstatus = - match status.gstatus with + let gstatus = + match status#stack with | [] -> assert false | s -> assert(gs <> []); let stack_locs = @@ -140,22 +147,23 @@ let focus_tac gs status = gs; (zero_pos gs, [], [], `FocusTag) :: deep_close gs s in - { status with gstatus = new_gstatus } + status#set_stack gstatus ;; let unfocus_tac status = - let new_gstatus = - match status.gstatus with + let gstatus = + match status#stack with | [] -> assert false - | ([], [], [], `FocusTag) :: s -> s - | _ -> fail (lazy "can't unfocus, some goals are still open") + | (g, [], [], `FocusTag) :: s when filter_open g = [] -> s + | _ as s -> fail (lazy ("can't unfocus, some goals are still open:\n"^ + Continuationals.Stack.pp s)) in - { status with gstatus = new_gstatus } + status#set_stack gstatus ;; let skip_tac status = - let new_gstatus = - match status.gstatus with + let gstatus = + match status#stack with | [] -> assert false | (gl, t, k, tag) :: s -> let gl = List.map switch_of_loc gl in @@ -164,17 +172,55 @@ let skip_tac status = else ([],t,k,tag) :: s in - { status with gstatus = new_gstatus } + status#set_stack gstatus +;; + +let block_tac l status = + List.fold_left (fun status tac -> tac status) status l ;; -let fold_tactic tac status = - match status.gstatus with + +let compare_statuses ~past ~present = + let _,_,past,_,_ = past#obj in + let _,_,present,_,_ = present#obj in + List.map fst (List.filter (fun (i,_) -> not(List.mem_assoc i past)) present), + List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past) +;; + + + +(* Exec and distribute_tac form a retraction pair: + 1) exec (distribute_tac low_tac) (s,i) = low_tac (s,i) + 2) tac [s]::G = G1::...::Gn::G' && G' is G with some goals closed => + distribute_tac (exec tac) [s]::G = (G1@...Gn)::G' + 3) tac G = distribute_tac (exec tac) G if + tac = distribute_tac lowtac + 4) atomic_tac t === distribute_tac (exec t) + + Note that executing an high tactic on a set of goals may be stronger + than executing the same tactic on those goals, but once at a time + (e.g. the tactic could perform a global analysis of the set of goals) +*) + +let exec tac (low_status : #lowtac_status) g = + let stack = [ [0,Open g], [], [], `NoTag ] in + let status = + (new NTacStatus.status low_status#obj stack)#set_estatus low_status + in + let status = tac status in + (low_status#set_estatus status)#set_obj status#obj +;; + +let distribute_tac tac (status : #tac_status) = + match status#stack with | [] -> assert false | (g, t, k, tag) :: s -> debug_print (lazy ("context length " ^string_of_int (List.length g))); let rec aux s go gc = function - | [] -> s, go, gc + | [] -> + debug_print (lazy "no selected goals"); + s, go, gc | loc :: loc_tl -> debug_print (lazy "inner eval tactical"); let s, go, gc = @@ -184,12 +230,14 @@ let fold_tactic tac status = match switch_of_loc loc with | Closed _ -> fail (lazy "cannot apply to a Closed goal") | Open n -> - let s, go', gc' = tac (s,n) in - s, (go @- gc') @+ go', gc @+ gc' + let sn = tac s n in + let go', gc' = compare_statuses ~past:s ~present:sn in + sn, ((go @+ [n]) @- gc') @+ go', gc @+ gc' in aux s go gc loc_tl in - let s0, go0, gc0 = status.istatus, [], [] in + let s0 = (new NTacStatus.status status#obj ())#set_estatus status in + let s0, go0, gc0 = s0, [], [] in let sn, gon, gcn = aux s0 go0 gc0 g in debug_print (lazy ("opened: " ^ String.concat " " (List.map string_of_int gon))); @@ -198,34 +246,432 @@ let fold_tactic tac status = let stack = (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s in - { gstatus = stack; istatus = sn } + ((status#set_stack stack)#set_obj(sn:>lowtac_status)#obj)#set_estatus sn +;; + +let atomic_tac htac : #tac_status as 'a -> 'a = distribute_tac (exec htac) ;; + +let repeat_tac t s = + let rec repeat t (status : #tac_status as 'a) : 'a = + try repeat t (t status) + with NTacStatus.Error _ -> status + in + atomic_tac (repeat t) s +;; + + +let try_tac tac status = + try + tac status + with NTacStatus.Error _ -> + status +;; + +let first_tac tacl status = + let res = + HExtlib.list_findopt + (fun tac _ -> try Some (tac status) with NTacStatus.Error _ -> None) tacl + in + match res with + | None -> fail (lazy "No tactics left") + | Some x -> x +;; + +let exact_tac t : 's tactic = distribute_tac (fun status goal -> + instantiate_with_ast status goal t) +;; + +let assumption_tac status = distribute_tac (fun status goal -> + let gty = get_goalty status goal in + let context = ctx_of gty in + let htac = + first_tac + (List.map (fun (name,_) -> exact_tac ("",0,(Ast.Ident (name,None)))) + context) + in + exec htac status goal) status +;; + +let find_in_context name context = + let rec aux acc = function + | [] -> raise Not_found + | (hd,_) :: tl when hd = name -> acc + | _ :: tl -> aux (acc + 1) tl + in + aux 1 context +;; + +let clear_tac names = + if names = [] then id_tac + else + distribute_tac (fun status goal -> + let goalty = get_goalty status goal in + let js = + List.map + (fun name -> + try find_in_context name (ctx_of goalty) + with Not_found -> + fail (lazy ("hypothesis '" ^ name ^ "' not found"))) + names + in + let n,h,metasenv,subst,o = status#obj in + let metasenv,subst,_,_ = NCicMetaSubst.restrict metasenv subst goal js in + status#set_obj (n,h,metasenv,subst,o)) ;; -let compare_menv ~past ~present = - List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i past)) present), - List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past) +let generalize0_tac args = + if args = [] then id_tac + else exact_tac ("",0,Ast.Appl (Ast.Implicit `JustOne :: args)) ;; -let apply t (status,goal) = - let uri,height,(metasenv as old_metasenv), subst,obj = status.pstatus in - let name,context,gty = List.assoc goal metasenv in - let metasenv, subst, lexicon_status, t = - GrafiteDisambiguate.disambiguate_nterm (Some gty) status.lstatus context metasenv subst t +let select0_tac ~where:(wanted,hyps,where) ~job = + let found, postprocess = + match job with + | `Substexpand argsno -> mk_in_scope, mk_out_scope argsno + | `Collect l -> (fun s t -> l := t::!l; mk_in_scope s t), mk_out_scope 1 + | `ChangeWith f -> f,(fun s t -> s, t) in - let subst, metasenv = - (goal, (name, context, t, gty)):: subst, - List.filter(fun (x,_) -> x <> goal) metasenv + distribute_tac (fun status goal -> + let goalty = get_goalty status goal in + let path = + match where with None -> NCic.Implicit `Term | Some where -> where + in + let status, newgoalctx = + List.fold_right + (fun (name,d as entry) (status,ctx) -> + try + let path = List.assoc name hyps in + match d with + NCic.Decl ty -> + let status,ty = + select_term status ~found ~postprocess (mk_cic_term ctx ty) + (wanted,path) in + let status,ty = term_of_cic_term status ty ctx in + status,(name,NCic.Decl ty)::ctx + | NCic.Def (bo,ty) -> + let status,bo = + select_term status ~found ~postprocess (mk_cic_term ctx bo) + (wanted,path) in + let status,bo = term_of_cic_term status bo ctx in + status,(name,NCic.Def (bo,ty))::ctx + with + Not_found -> status, entry::ctx + ) (ctx_of goalty) (status,[]) + in + let status, newgoalty = + select_term status ~found ~postprocess goalty (wanted,path) in + (* WARNING: the next two lines simply change the context of newgoalty + from the old to the new one. Otherwise mk_meta will do that herself, + calling relocate that calls delift. However, newgoalty is now + ?[out_scope] and thus the delift would trigger the special unification + case, which is wrong now :-( *) + let status,newgoalty = term_of_cic_term status newgoalty (ctx_of goalty) in + let newgoalty = mk_cic_term newgoalctx newgoalty in + + let status, instance = + mk_meta status newgoalctx (`Decl newgoalty) `IsTerm + in + instantiate status goal instance) +;; + +let select_tac ~where ~job move_down_hyps = + let (wanted,hyps,where) = GrafiteDisambiguate.disambiguate_npattern where in + let path = + match where with None -> NCic.Implicit `Term | Some where -> where in + if not move_down_hyps then + select0_tac ~where:(wanted,hyps,Some path) ~job + else + let path = + List.fold_left + (fun path (name,path_name) -> NCic.Prod ("_",path_name,path)) + path (List.rev hyps) + in + block_tac [ + generalize0_tac (List.map (fun (name,_) -> Ast.Ident (name,None)) hyps); + select0_tac ~where:(wanted,[],Some path) ~job; + clear_tac (List.map fst hyps) ] +;; + +let generalize_tac ~where = + let l = ref [] in + block_tac [ + select_tac ~where ~job:(`Collect l) true; + (fun s -> distribute_tac (fun status goal -> + let goalty = get_goalty status goal in + let status,canon,rest = + match !l with + [] -> + (match where with + _,_,(None,_,_) -> fail (lazy "No term to generalize") + | txt,txtlen,(Some what,_,_) -> + let status, what = + disambiguate status (ctx_of goalty) (txt,txtlen,what) None + in + status,what,[] + ) + | he::tl -> status,he,tl in + let status = + List.fold_left + (fun s t -> unify s (ctx_of goalty) canon t) status rest in + let status, canon = term_of_cic_term status canon (ctx_of goalty) in + instantiate status goal + (mk_cic_term (ctx_of goalty) (NCic.Appl [NCic.Implicit `Term ; canon ])) + ) s) ] +;; + +let cut_tac t = + block_tac [ + exact_tac ("",0, Ast.Appl [Ast.Implicit `JustOne; Ast.Implicit `JustOne]); + branch_tac; + pos_tac [3]; exact_tac t; + shift_tac; pos_tac [2]; skip_tac; + merge_tac ] +;; + +let lapply_tac (s,n,t) = + exact_tac (s,n, Ast.Appl [Ast.Implicit `JustOne; t]) +;; + +let reduce_tac ~reduction ~where = + let change status t = + match reduction with + | `Normalize perform_delta -> + normalize status + ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t + | `Whd perform_delta -> + whd status + ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t + in + let where = GrafiteDisambiguate.disambiguate_npattern where in + select0_tac ~where ~job:(`ChangeWith change) +;; + +let change_tac ~where ~with_what = + let change status t = + let status, ww = disambiguate status (ctx_of t) with_what None in + let status = unify status (ctx_of t) t ww in + status, ww + in + let where = GrafiteDisambiguate.disambiguate_npattern where in + select0_tac ~where ~job:(`ChangeWith change) +;; + +let letin_tac ~where ~what:(_,_,w) name = + block_tac [ + select_tac ~where ~job:(`Substexpand 1) true; + exact_tac + ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit `JustOne)); + ] +;; + +let apply_tac (s,n,t) = + let t = Ast.Appl [t; Ast.Implicit `Vector] in + exact_tac (s,n,t) +;; + +type indtyinfo = { + rightno: int; + leftno: int; + consno: int; + lefts: NCic.term list; + rights: NCic.term list; + reference: NReference.reference; + } +;; + +let ref_of_indtyinfo iti = iti.reference;; + +let analyze_indty_tac ~what indtyref = + distribute_tac (fun status goal -> + let goalty = get_goalty status goal in + let status, what = disambiguate status (ctx_of goalty) what None in + let status, ty_what = typeof status (ctx_of what) what in + let status, (r,consno,lefts,rights) = analyse_indty status ty_what in + let leftno = List.length lefts in + let rightno = List.length rights in + indtyref := Some { + rightno = rightno; leftno = leftno; consno = consno; + lefts = lefts; rights = rights; reference = r; + }; + exec id_tac status goal) +;; + +let sort_of_goal_tac sortref = distribute_tac (fun status goal -> + let goalty = get_goalty status goal in + let status,sort = typeof status (ctx_of goalty) goalty in + let status, sort = fix_sorts status sort in + let status, sort = term_of_cic_term status sort (ctx_of goalty) in + sortref := sort; + status) +;; + +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 (NCic.Rel 1) in + atomic_tac (block_tac [ + analyze_indty_tac ~what indtyinfo; + (fun s -> select_tac + ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1)) true s); + sort_of_goal_tac sort; + (fun status -> + let ity = HExtlib.unopt !indtyinfo in + let NReference.Ref (uri, _) = ity.reference in + let name = + NUri.name_of_uri uri ^ "_" ^ + snd (NCicElim.ast_of_sort + (match !sort with NCic.Sort x -> x | _ -> assert false)) + in + let eliminator = + let _,_,w = what in + Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ] + in + exact_tac ("",0,eliminator) status) ]) +;; + +let rewrite_tac ~dir ~what:(_,_,what) ~where status = + let sortref = ref (NCic.Rel 1) in + let status = sort_of_goal_tac sortref status in + let suffix = "_" ^ snd (NCicElim.ast_of_sort + (match !sortref with NCic.Sort x -> x | _ -> assert false)) + in + let name = + match dir with + `LeftToRight -> "eq" ^ suffix ^ "_r" + | `RightToLeft -> "eq" ^ suffix + in + block_tac + [ select_tac ~where ~job:(`Substexpand 1) true; + exact_tac + ("",0, + Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list (Ast.Implicit `JustOne) 5@ + [what]))] status +;; + +let intro_tac name = + block_tac + [ exact_tac + ("",0,(Ast.Binder (`Lambda, + (Ast.Ident (name,None),None),Ast.Implicit `JustOne))); + if name = "_" then clear_tac [name] else id_tac ] +;; + +let cases ~what status goal = + let gty = get_goalty status goal in + let status, what = disambiguate status (ctx_of gty) what None in + let status, ty = typeof status (ctx_of what) what in + let status, (ref, consno, _, _) = analyse_indty status ty in + let status, what = term_of_cic_term status what (ctx_of gty) in + let t = + NCic.Match (ref,NCic.Implicit `Term, what, + HExtlib.mk_list (NCic.Implicit `Term) consno) in - let open_goals, closed_goals = compare_menv ~past:old_metasenv ~present:metasenv in - let new_pstatus = uri,height,metasenv,subst,obj in + instantiate status goal (mk_cic_term (ctx_of gty) t) +;; + +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 [ + analyze_indty_tac ~what indtyinfo; + (fun s -> select_tac + ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1))true s); + distribute_tac (cases ~what) ]) +;; - prerr_endline ("termine disambiguato: " ^ NCicPp.ppterm ~context ~metasenv ~subst t); - prerr_endline ("menv:" ^ NCicPp.ppmetasenv ~subst metasenv); - prerr_endline ("subst:" ^ NCicPp.ppsubst subst ~metasenv); - prerr_endline "fine napply"; +let case1_tac name = + let name = if name = "_" then "_clearme" else name in + block_tac [ intro_tac name; + cases_tac + ~where:("",0,(None,[],None)) + ~what:("",0,Ast.Ident (name,None)); + if name = "_clearme" then clear_tac ["_clearme"] else id_tac ] +;; + +let constructor_tac ?(num=1) ~args = distribute_tac (fun status goal -> + if num < 1 then fail (lazy "constructor numbers begin with 1"); + let gty = get_goalty status goal in + let status, (r,_,_,_) = analyse_indty status gty in + let ref = NReference.mk_constructor num r in + let t = + if args = [] then Ast.NRef ref else + Ast.Appl (HExtlib.list_concat ~sep:[Ast.Implicit `Vector] + ([Ast.NRef ref] :: List.map (fun _,_,x -> [x]) args)) + in + exec (apply_tac ("",0,t)) status goal) +;; - { lstatus = lexicon_status; pstatus = new_pstatus }, open_goals, closed_goals +let assert0_tac (hyps,concl) = distribute_tac (fun status goal -> + let gty = get_goalty status goal in + let eq status ctx t1 t2 = + let status,t1 = disambiguate status ctx t1 None in + let status,t1 = apply_subst status ctx t1 in + let status,t1 = term_of_cic_term status t1 ctx in + let t2 = mk_cic_term ctx t2 in + let status,t2 = apply_subst status ctx t2 in + let status,t2 = term_of_cic_term status t2 ctx in + prerr_endline ("COMPARING: " ^ NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:ctx t1 ^ " vs " ^ NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:ctx t2); + assert (t1=t2); + status + in + let status,gty' = term_of_cic_term status gty (ctx_of gty) in + let status = eq status (ctx_of gty) concl gty' in + let status,_ = + List.fold_right2 + (fun (id1,e1) ((id2,e2) as item) (status,ctx) -> + assert (id1=id2 || (prerr_endline (id1 ^ " vs " ^ id2); false)); + match e1,e2 with + `Decl t1, NCic.Decl t2 -> + let status = eq status ctx t1 t2 in + status,item::ctx + | `Def (b1,t1), NCic.Def (b2,t2) -> + let status = eq status ctx t1 t2 in + let status = eq status ctx b1 b2 in + status,item::ctx + | _ -> assert false + ) hyps (ctx_of gty) (status,[]) + in + exec id_tac status goal) ;; -let apply_tac t = fold_tactic (apply t) ;; +let assert_tac seqs status = + match status#stack with + | [] -> assert false + | (g,_,_,_) :: s -> + assert (List.length g = List.length seqs); + (match seqs with + [] -> id_tac + | [seq] -> assert0_tac seq + | _ -> + block_tac + ((branch_tac ~force:false):: + HExtlib.list_concat ~sep:[shift_tac] + (List.map (fun seq -> [assert0_tac seq]) seqs)@ + [merge_tac]) + ) status +;; +let inversion_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 (NCic.Rel 1) in + atomic_tac (block_tac [ + analyze_indty_tac ~what indtyinfo; + (fun s -> select_tac + ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1)) true s); + sort_of_goal_tac sort; + (fun status -> + let ity = HExtlib.unopt !indtyinfo in + let NReference.Ref (uri, _) = ity.reference in + let name = + NUri.name_of_uri uri ^ "_inv_" ^ + snd (NCicElim.ast_of_sort + (match !sort with NCic.Sort x -> x | _ -> assert false)) + in + let eliminator = + let _,_,w = what in + Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ] + in + exact_tac ("",0,eliminator) status) ]) +;;