Tactic reduce got rid of. Use normalize, instead.

[helm.git] / helm / software / components / tactics / tactics.mli

diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli
index 69f415ee14f8bfb4e122534f941e75df3e67d7b9..0a0a2e0d6b39cd3070a16a010eaad96aaf374474 100644 (file)
--- a/helm/software/components/tactics/tactics.mli
+++ b/helm/software/components/tactics/tactics.mli
@@ -79,7 +79,6 @@ val letin :
   Cic.term -> ProofEngineTypes.tactic
 val normalize :
   pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
-val reduce : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
 val reflexivity : ProofEngineTypes.tactic
 val replace :
   pattern:ProofEngineTypes.lazy_pattern ->