parameter sintax added to axiom statement

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

diff --git a/helm/software/components/tactics/variousTactics.mli b/helm/software/components/tactics/variousTactics.mli
index 35576326eb2dbc2f6ffa1e0f4b7adb6744908acc..3ce6c47e8a400b95118a10d687161a58ad81edcc 100644 (file)
--- 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
-