X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FvariousTactics.ml;h=604307cd35cb662b16631efb40cc16044b3d7a00;hb=331dc1783c8572be9d5c7c0ba11fa2995539bbf6;hp=615cf43b4930c954b4fc3f187138610d7c9c8091;hpb=700e8726d8b97f923ed7e02f1146a9787bde2333;p=helm.git

diff --git a/helm/gTopLevel/variousTactics.ml b/helm/gTopLevel/variousTactics.ml
index 615cf43b4..604307cd3 100644
--- a/helm/gTopLevel/variousTactics.ml
+++ b/helm/gTopLevel/variousTactics.ml
@@ -65,6 +65,9 @@ let assumption_tac ~status:(proof,goal)=
 
 (* ANCORA DA DEBUGGARE *)
 
+(* 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 *)
 let generalize_tac ~term ~status:((proof,goal) as status) =
   let module C = Cic in
   let module P = PrimitiveTactics in
@@ -82,7 +85,7 @@ let generalize_tac ~term ~status:((proof,goal) as status) =
             ~what:term 
             ~with_what:(C.Rel 1) (* C.Name "dummy_for_gen" *)  
             ~where:ty)
-          )))	
+        )))	
       ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac]
       ~status
 ;;