]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_tactics/nTactics.mli
tentative subst-sexpand and change
[helm.git] / helm / software / components / ng_tactics / nTactics.mli
index f9747e824de9a066b122df1083cf606c2b8d5ef4..29b7613a502878ef702cfc9b3378e75192f04ded 100644 (file)
@@ -42,6 +42,7 @@ val distribute_tac: lowtactic -> tactic
 val block_tac: tactic list -> tactic
 
 val apply_tac: tactic_term -> tactic
+val change_tac: tactic_term -> tactic_term -> tactic
 
 
 val pp_tac_status: tac_status -> unit