the passive set and passive list are expected to have the same cardinality, that...

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

diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml
index 16aa6d3b2d5925a10b1ab3bf7e47583885365c2f..6eae445313304922677231b3aa0f518f108fb9d4 100644 (file)
--- 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 =