debug=false

[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..d6a6c91b9d8e60ad78d5b95fea237865869a37af 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)
  =
@@ -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