This commit makes ProofEngineHelpers.select reach its full potentials.

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

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 2e6810387455602779d23bb9642ae29e2de2c750..73309c43ecfb387cf2f901700c52461f26ad0b45 100644 (file)
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -66,7 +66,7 @@ let assumption_tac =
 exception UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly;;
 exception TheSelectedTermsMustLiveInTheGoalContext
 exception AllSelectedTermsMustBeConvertible;;
-exception CannotGeneralizeInHypotheses;;
+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
@@ -80,15 +80,16 @@ 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
+    assert (selected_hyps = []);
     let typ,term =
      match terms_with_context, term with
         [], None ->