X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FequalityTactics.mli;h=1aa48173c710d34a62eea4b1f2fa30555b3b57a4;hb=433d9c9612c1557e03a549e004c796c1137d4b4a;hp=52f2f20430559eb71a2bc1638aa6c7849bb16d7b;hpb=5f00ef380aafdaae93a40a3a47491d43ec9c3a62;p=helm.git

diff --git a/helm/software/components/tactics/equalityTactics.mli b/helm/software/components/tactics/equalityTactics.mli
index 52f2f2043..1aa48173c 100644
--- a/helm/software/components/tactics/equalityTactics.mli
+++ b/helm/software/components/tactics/equalityTactics.mli
@@ -40,8 +40,3 @@ val replace_tac:
 val reflexivity_tac: ProofEngineTypes.tactic
 val symmetry_tac: ProofEngineTypes.tactic
 val transitivity_tac: term:Cic.term -> ProofEngineTypes.tactic
-
-(* FG *)
-
-(* rewrites and clears all simple equalities in the context *)
-val subst_tac: ProofEngineTypes.tactic