]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/matitaMathView.ml
More statuses converted to objects.
[helm.git] / helm / software / matita / matitaMathView.ml
index e93ac4f3cf1bddb4adb41c57c79e81e41a65b498..22ad1e4cf144c6e9ed8fe4fb037d94862b7fa540 100644 (file)
@@ -1334,7 +1334,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
 
     method private home () =
       self#_showMath;
-      match self#script#grafite_status.proof_status with
+      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 =
@@ -1348,7 +1348,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
          in
           self#_loadObj obj
       | _ ->
-        match self#script#grafite_status.ng_status with
+        match self#script#grafite_status#ng_status with
            ProofMode tstatus -> self#_loadNObj tstatus#obj
          | _ -> self#blank ()