paths trough terms implemented with a nice hack :)

[helm.git] / helm / ocaml / tactics / tactics.mli

diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli
index b69e43e88328ebcec45200a7303ecc0686e7d742..a91985290838195bfcd4a9813a0d5de8b5c674a9 100644 (file)
--- 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