From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 30 Jun 2005 09:07:35 +0000 (+0000)
Subject: Obsolete comment removed.
X-Git-Tag: PRE_GETTER_STORAGE~106
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=974e4dee51a81052677792c3ee242ee3396c2d8b;p=helm.git

Obsolete comment removed.
---

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