version 0.7.1

[helm.git] / helm / ocaml / tactics / variousTactics.ml

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 2e6810387455602779d23bb9642ae29e2de2c750..8bbe05dcb77b1cc78f19e857033aec95e3bee5a2 100644 (file)
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -66,29 +66,26 @@ 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:[])
  pattern
  =
+(*
   let module PET = ProofEngineTypes in
   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 ->
@@ -146,4 +143,5 @@ let generalize_tac
        status
  in
   PET.mk_tactic (generalize_tac mk_fresh_name_callback ~pattern)
+*) assert false
 ;;