X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FequalityTactics.ml;h=6eae445313304922677231b3aa0f518f108fb9d4;hb=0e3324ad8e6a552ee89f02371412f7bc2e83379f;hp=16aa6d3b2d5925a10b1ab3bf7e47583885365c2f;hpb=55c78a59b2127ecead99bb814a3ca519f8087053;p=helm.git

diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml
index 16aa6d3b2..6eae44531 100644
--- a/helm/software/components/tactics/equalityTactics.ml
+++ b/helm/software/components/tactics/equalityTactics.ml
@@ -160,7 +160,7 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality =
   let t1 = CicMetaSubst.apply_subst subst t1 in
   let t2 = CicMetaSubst.apply_subst subst t2 in
   let ty = CicMetaSubst.apply_subst subst ty 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 equality = CicMetaSubst.apply_subst subst equality in
   let abstr_gty =
@@ -238,7 +238,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
   let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
   let with_what, metasenv, u = with_what context metasenv u in
   let with_what = CicMetaSubst.apply_subst subst with_what 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 status = (uri,metasenv,_subst,pbo,pty, attrs),goal in
   let ty_of_with_what,u =