X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Ftactics%2Ftactics.mli;h=a91985290838195bfcd4a9813a0d5de8b5c674a9;hb=acf29bdbdcdc6ad8c2d9d27e8a47500981b605cd;hp=b69e43e88328ebcec45200a7303ecc0686e7d742;hpb=c677064eeb73cd930a5651b884f79bbe6fc5694a;p=helm.git

diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli
index b69e43e88..a91985290 100644
--- a/helm/ocaml/tactics/tactics.mli
+++ b/helm/ocaml/tactics/tactics.mli
@@ -63,3 +63,6 @@ val transitivity : term:Cic.term -> ProofEngineTypes.tactic
 val whd :
   also_in_hypotheses:bool ->
   terms:Cic.term list option -> ProofEngineTypes.tactic
+val normalize :
+  also_in_hypotheses:bool ->
+  terms:Cic.term list option -> ProofEngineTypes.tactic