X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fcompose.ml;h=e009010a7648980a9d979df0bd65b7edc781adc4;hb=da3031c3a830df0aaab4f57b63689a1b20d7ab89;hp=6bc3dd0fa2160dac8117a9d64f52f94f4a1870b2;hpb=81d0d5a3aad863b991996c008f5c19076e771dbb;p=helm.git

diff --git a/helm/software/components/tactics/compose.ml b/helm/software/components/tactics/compose.ml
index 6bc3dd0fa..e009010a7 100644
--- 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);