Corrected type for bag

[helm.git] / helm / software / matita / matitaMathView.ml

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index e93ac4f3cf1bddb4adb41c57c79e81e41a65b498..f00ea1a0fe89be0f6859ce7d91141579f5314534 100644 (file)
--- 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;
@@ -1334,7 +1335,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,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