X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FprimitiveTactics.ml;h=d6a6c91b9d8e60ad78d5b95fea237865869a37af;hb=63e7ef727ce32552106c4d8f3030fd264532fffe;hp=db8fe4376686468c076b1ab41995a9c0e5ff5af2;hpb=ed5c4e15429c37bef0f59dfd7160f6883586ed0f;p=helm.git

diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml
index db8fe4376..d6a6c91b9 100644
--- a/helm/software/components/tactics/primitiveTactics.ml
+++ b/helm/software/components/tactics/primitiveTactics.ml
@@ -366,6 +366,12 @@ let apply_tac ~term =
  in
   PET.mk_tactic (apply_tac ~term)
 
+let applyP_tac ~term =
+   let applyP_tac status =
+      let res = PET.apply_tactic (apply_tac ~term) status in res
+   in
+   PET.mk_tactic applyP_tac
+
 let intros_tac ?howmany ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ()=
  let intros_tac (proof, goal)
  =
@@ -631,7 +637,7 @@ let generalize_tac
       ~conjecture ~pattern in
     let context = CicMetaSubst.apply_subst_context subst context in
     let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
-    let pbo = CicMetaSubst.apply_subst subst pbo in
+    let pbo = lazy (CicMetaSubst.apply_subst subst (Lazy.force pbo)) in
     let pty = CicMetaSubst.apply_subst subst pty in
     let term =
      match term with