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