dependences update

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

diff --git a/helm/software/components/tactics/equalityTactics.mli b/helm/software/components/tactics/equalityTactics.mli
index 52f2f20430559eb71a2bc1638aa6c7849bb16d7b..1aa48173c710d34a62eea4b1f2fa30555b3b57a4 100644 (file)
--- 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