X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FproofEngineHelpers.ml;h=fc508f0c11a33b85df8795ab5c63e487b3214dcb;hb=0e3324ad8e6a552ee89f02371412f7bc2e83379f;hp=e45c13257d54003e2dbee36171e84463417127e1;hpb=36842ee77114d2fa896d7ffd2333c07cff22b053;p=helm.git

diff --git a/helm/software/components/tactics/proofEngineHelpers.ml b/helm/software/components/tactics/proofEngineHelpers.ml
index e45c13257..fc508f0c1 100644
--- a/helm/software/components/tactics/proofEngineHelpers.ml
+++ b/helm/software/components/tactics/proofEngineHelpers.ml
@@ -56,7 +56,7 @@ let subst_meta_in_proof proof meta term newmetasenv =
          i,canonical_context',(subst_in ty)
       ) metasenv'
     in
-     let bo' = subst_in bo in
+     let bo' = lazy (subst_in (Lazy.force bo)) in
      (* Metavariables can appear also in the *statement* of the theorem
       * since the parser does not reject as statements terms with
       * metavariable therein *)
@@ -79,7 +79,7 @@ let subst_meta_in_proof proof meta term newmetasenv =
 let subst_meta_and_metasenv_in_proof proof meta subst newmetasenv =
  let (uri,_,initial_subst,bo,ty, attrs) = proof in
   let subst_in = CicMetaSubst.apply_subst subst in
-  let bo' = subst_in bo in
+  let bo' = lazy (subst_in (Lazy.force bo)) in
   (* Metavariables can appear also in the *statement* of the theorem
    * since the parser does not reject as statements terms with
    * metavariable therein *)