+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
+ 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 elim_tac ~what ~where =
+ let indtyinfo = ref None in
+ let sort = ref None in
+ let compute_goal_sort_tac = distribute_tac (fun status goal ->
+ let goalty = get_goalty status goal in
+ let status, goalsort = typeof status (ctx_of goalty) goalty in
+ sort := Some goalsort;
+ exec id_tac status goal)
+ in
+ atomic_tac (block_tac [
+ analyze_indty_tac ~what indtyinfo;
+ (fun s -> select_tac
+ ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1)) true s);
+ compute_goal_sort_tac;
+ (fun status ->
+ let sort = HExtlib.unopt !sort in
+ let ity = HExtlib.unopt !indtyinfo in
+ let NReference.Ref (uri, _) = ity.reference in
+ let status, sort = term_of_cic_term status sort (ctx_of sort) in
+ let name = NUri.name_of_uri uri ^
+ match sort with
+ | NCic.Sort NCic.Prop -> "_ind"
+ | NCic.Sort NCic.Type u ->
+ "_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 =