- Procedural: bug fix in rendering the application: we must handle the

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

diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml
index db8fe4376686468c076b1ab41995a9c0e5ff5af2..0fa4ebaec60a335ee0be727e741e42fac035cf83 100644 (file)
--- 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)
  =