Hypotheses patterns for elim implemented. No more need to generalize in advance.

[helm.git] / helm / software / components / tactics / compose.ml

diff --git a/helm/software/components/tactics/compose.ml b/helm/software/components/tactics/compose.ml
index 6bc3dd0fa2160dac8117a9d64f52f94f4a1870b2..e009010a7648980a9d979df0bd65b7edc781adc4 100644 (file)
--- a/helm/software/components/tactics/compose.ml
+++ b/helm/software/components/tactics/compose.ml
@@ -125,7 +125,7 @@ let compose_core t2 t1 (proof, goal) =
         in
         let proof, gl = 
           ProofEngineTypes.apply_tactic
-            (VariousTactics.generalize_tac (Some (lazy_of t), [], None))
+            (PrimitiveTactics.generalize_tac (Some (lazy_of t), [], None))
             (proof,goal)
         in
         assert(List.length gl = 1);