From 974e4dee51a81052677792c3ee242ee3396c2d8b Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 30 Jun 2005 09:07:35 +0000
Subject: [PATCH] Obsolete comment removed.

---
 helm/ocaml/tactics/variousTactics.ml | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 51e59961d..e2003f48d 100644
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -68,10 +68,6 @@ exception TheSelectedTermsMustLiveInTheGoalContext
 exception AllSelectedTermsMustBeConvertible;;
 exception GeneralizationInHypothesesNotImplementedYet;;
 
-(* serve una funzione che cerchi nel ty dal basso a partire da term, i lambda
-e li aggiunga nel context, poi si conta la lunghezza di questo nuovo
-contesto e si lifta di tot... COSA SIGNIFICA TUTTO CIO'?????? *)
-
 let generalize_tac 
  ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
  pattern
-- 
2.39.2