X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMathView.ml;h=63cf77a16e356352294078aa27e5651e7213e54c;hb=d5b0c5c4409e789df8629943de2344a54b64686b;hp=e6c26179132205f9028779dc0a8d7868b9271f43;hpb=65aa5d46b240da7b91e57fc74890d8544aa479c3;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 ()