X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Ftactics%2FvariousTactics.ml;h=8bbe05dcb77b1cc78f19e857033aec95e3bee5a2;hb=5d5e328a05ed70fcf565aef8f92b7ec87b2740f2;hp=51e59961d159ac4617de0c44b9219ed51503133d;hpb=4a60de346329c7b198f1bc94072131715827a1ff;p=helm.git

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 51e59961d..8bbe05dcb 100644
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -68,14 +68,11 @@ 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
  =
+(*
   let module PET = ProofEngineTypes in
   let generalize_tac mk_fresh_name_callback
        ~pattern:(term,hyps_pat,concl_pat) status
@@ -146,4 +143,5 @@ let generalize_tac
        status
  in
   PET.mk_tactic (generalize_tac mk_fresh_name_callback ~pattern)
+*) assert false
 ;;