+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 = term_of_cic_term status sort (ctx_of goalty) in
+ sortref := sort;
+ 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 =
+ match !sortref with
+ | NCic.Sort NCic.Prop -> "_ind"
+ | NCic.Sort NCic.Type u ->
+ "_rect_" ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] !sortref
+ | _ -> assert false
+ in