X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FvariousTactics.mli;h=3ce6c47e8a400b95118a10d687161a58ad81edcc;hb=152966d146348c74302df64e12c7644c00eb447e;hp=35576326eb2dbc2f6ffa1e0f4b7adb6744908acc;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/tactics/variousTactics.mli b/helm/software/components/tactics/variousTactics.mli
index 35576326e..3ce6c47e8 100644
--- a/helm/software/components/tactics/variousTactics.mli
+++ b/helm/software/components/tactics/variousTactics.mli
@@ -24,12 +24,4 @@
  * http://cs.unibo.it/helm/.
  *)
 
-exception AllSelectedTermsMustBeConvertible;;
-
 val assumption_tac: ProofEngineTypes.tactic
-
-val generalize_tac:
- ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
- ProofEngineTypes.lazy_pattern ->
-   ProofEngineTypes.tactic
-