X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FreductionTactics.mli;h=a4cf407f08fc103a26a977b9895ad1179c068b90;hb=b0f879da074adb838681869bf401c97d0a860c6b;hp=97418b4da214a23bd079da031691204bfd976a29;hpb=3066e4dcb7270a5eb20020a91d45da9eb87e2f2e;p=helm.git

diff --git a/helm/gTopLevel/reductionTactics.mli b/helm/gTopLevel/reductionTactics.mli
index 97418b4da..a4cf407f0 100644
--- a/helm/gTopLevel/reductionTactics.mli
+++ b/helm/gTopLevel/reductionTactics.mli
@@ -26,3 +26,5 @@
 val simpl_tac: ProofEngineTypes.tactic
 val reduce_tac: ProofEngineTypes.tactic
 val whd_tac: ProofEngineTypes.tactic
+val fold_tac:
+ also_in_hypotheses:bool -> term:Cic.term -> ProofEngineTypes.tactic