X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMathView.ml;h=63cf77a16e356352294078aa27e5651e7213e54c;hb=45a9e84c12f57e5473eccc6f611cdbb343998d5d;hp=e6c26179132205f9028779dc0a8d7868b9271f43;hpb=99feea74c16b4801a2b1596d5e48e27224ffbfaa;p=helm.git

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index e6c261791..63cf77a16 100644
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -1154,11 +1154,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       match self#script#grafite_status.proof_status with
       | Proof  (uri, metasenv, _subst, bo, ty, attrs) ->
           let name = UriManager.name_of_uri (HExtlib.unopt uri) in
-          let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], attrs) in
+          let obj = Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs) in
           self#_loadObj obj
       | Incomplete_proof { proof = (uri, metasenv, _subst, bo, ty, attrs) } ->
           let name = UriManager.name_of_uri (HExtlib.unopt uri) in
-          let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], attrs) in
+          let obj = Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs) in
           self#_loadObj obj
       | _ -> self#blank ()