X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FprimitiveTactics.ml;h=d6a6c91b9d8e60ad78d5b95fea237865869a37af;hb=63e7ef727ce32552106c4d8f3030fd264532fffe;hp=0fa4ebaec60a335ee0be727e741e42fac035cf83;hpb=3b8d99d5fdb79a5d979a8e200a4a4307fe362009;p=helm.git

diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml
index 0fa4ebaec..d6a6c91b9 100644
--- a/helm/software/components/tactics/primitiveTactics.ml
+++ b/helm/software/components/tactics/primitiveTactics.ml
@@ -637,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