-let return ~orig status =
- let _,_,past,_,_ = orig.pstatus in
- let _,_,present,_,_ = status.pstatus in
- let open_goals, closed_goals = compare_menv ~past ~present in
- status, open_goals, closed_goals
+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) = exact_tac (s,n,Ast.Appl [t; Ast.Implicit `Vector]);;
+
+type indtyinfo = {
+ rightno: int;
+ leftno: int;
+ consno: int;
+ lefts: NCic.term list;
+ rights: NCic.term list;
+ reference: NReference.reference;
+ }
+;;
+
+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 =
+ let _,_,w = what in
+ Ast.Appl(Ast.Ident(name,None)::holes @ [ w ])
+ in
+ exact_tac ("",0,eliminator) status) ])