X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FprimitiveTactics.ml;h=0fa4ebaec60a335ee0be727e741e42fac035cf83;hb=1c2cadee5d666f0e31085a4ff358d667379c4f25;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..0fa4ebaec 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)
  =