X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FvariousTactics.ml;h=e2003f48d4ab1b2b437393245b5b3aa8d9fa4476;hb=536e560bab5e6170f84713b9059ea37527a075b2;hp=2e6810387455602779d23bb9642ae29e2de2c750;hpb=80fc89019bcb7fb7e0e1fb8bb111b708be49d19f;p=helm.git

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 2e6810387..e2003f48d 100644
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -66,11 +66,7 @@ let assumption_tac =
 exception UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly;;
 exception TheSelectedTermsMustLiveInTheGoalContext
 exception AllSelectedTermsMustBeConvertible;;
-exception CannotGeneralizeInHypotheses;;
-
-(* 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'?????? *)
+exception GeneralizationInHypothesesNotImplementedYet;;
 
 let generalize_tac 
  ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
@@ -80,15 +76,15 @@ let generalize_tac
   let generalize_tac mk_fresh_name_callback
        ~pattern:(term,hyps_pat,concl_pat) status
   =
-   if hyps_pat <> [] then raise CannotGeneralizeInHypotheses ;
+   if hyps_pat <> [] then raise GeneralizationInHypothesesNotImplementedYet;
    let (proof, goal) = status in
    let module C = Cic in
    let module P = PrimitiveTactics in
    let module T = Tacticals in
     let _,metasenv,_,_ = proof in
-    let _,context,ty = CicUtil.lookup_meta goal metasenv in
-    let terms_with_context =
-     ProofEngineHelpers.select ~context ~term:ty ~pattern:(term,concl_pat) in
+    let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
+    let selected_hyps,terms_with_context =
+     ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in
     let typ,term =
      match terms_with_context, term with
         [], None ->