-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) ])
-;;