+and subst_tac ~map ~term ~direction ~where ~continuation =
+ let fail_tactic = continuation ~map in
+ let subst_tac status =
+ let term = relocate_term map term in
+ let tactic = match where with
+ | None ->
+ let pattern = PET.conclusion_pattern None in
+ let tactic = ET.rewrite_tac ~direction ~pattern term [] in
+ T.then_ ~start:(T.try_tactic ~tactic)
+ ~continuation:fail_tactic
+ | Some name ->
+ let pattern = None, [name, PET.hole], None in
+ let start = ET.rewrite_tac ~direction ~pattern term [] in
+ let continuation =
+ destruct ~first_time:false ~term:(C.Rel 1) ~map:id
+ ~continuation:(after2 continuation succ map)
+ in
+ T.if_ ~start ~continuation ~fail:fail_tactic
+ in
+ PET.apply_tactic tactic status
+ in
+ PET.mk_tactic subst_tac
+
+(* ~term vive nel contesto della tattica una volta ~mappato
+ * ~continuation riceve la mappa assoluta
+ *)
+and destruct ~first_time ~map ~term ~continuation =