X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMathView.ml;fp=helm%2Fsoftware%2Fmatita%2FmatitaMathView.ml;h=f00ea1a0fe89be0f6859ce7d91141579f5314534;hb=779859f7a9e317e378d258897c289f447adea7ad;hp=22ad1e4cf144c6e9ed8fe4fb037d94862b7fa540;hpb=9a7c77e5c29d764109a104aa629761ba90cb511c;p=helm.git

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index 22ad1e4cf..f00ea1a0f 100644
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -798,7 +798,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
           self#script#setGoal (Some (goal_of_switch goal_switch));
           self#render_page ~page ~goal_switch))
 
-    method nload_sequents (status : NTacStatus.tac_status) =
+    method nload_sequents : 'status. #NTacStatus.tac_status as 'status -> unit
+    = fun status ->
      let _,_,metasenv,subst,_ = status#obj in
       _metasenv <- `New (metasenv,subst);
       pages <- 0;
@@ -1348,8 +1349,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
          in
           self#_loadObj obj
       | _ ->
-        match self#script#grafite_status#ng_status with
-           ProofMode tstatus -> self#_loadNObj tstatus#obj
+        match self#script#grafite_status#ng_mode with
+           `ProofMode -> self#_loadNObj self#script#grafite_status#obj
          | _ -> self#blank ()
 
       (** loads a cic uri from the environment