X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaMathView.ml;h=9990805ad7614ce2ab407700bb8f27363a3ae2d5;hb=f9f775a550264a8dc9ce7ea9a48b79892a122c3c;hp=280ade3ee11ac559fa3494d0fe2e4d81175a8bb8;hpb=2a59f55f4625ebabb02aefc3cb8c8842040be554;p=helm.git

diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml
index 280ade3ee..9990805ad 100644
--- a/matita/matita/matitaMathView.ml
+++ b/matita/matita/matitaMathView.ml
@@ -620,7 +620,7 @@ object (self)
   val mutable current_mathml = None
 
   method nload_sequent:
-   'status. #LexiconTypes.status as 'status -> NCic.metasenv ->
+   'status. #ApplyTransformation.status as 'status -> NCic.metasenv ->
      NCic.substitution -> int -> unit
    = fun status metasenv subst metano ->
     let sequent = List.assoc metano metasenv in
@@ -637,7 +637,7 @@ object (self)
     self#load_root ~root:txt
 
   method load_nobject :
-   'status. #LexiconTypes.status as 'status -> NCic.obj -> unit
+   'status. #ApplyTransformation.status as 'status -> NCic.obj -> unit
    = fun status obj ->
     let txt = ApplyTransformation.ntxt_of_cic_object ~map_unicode_to_tex:false
     80 status obj in
@@ -727,8 +727,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
       _metasenv <- `Old []; 
       self#script#setGoal None
 
-    method nload_sequents : 'status. #NTacStatus.tac_status as 'status -> unit
-    = fun (status : #NTacStatus.tac_status) ->
+    method nload_sequents : 'status. #GrafiteTypes.status as 'status -> unit
+    = fun (status : #GrafiteTypes.status) ->
      let _,_,metasenv,subst,_ = status#obj in
       _metasenv <- `New (metasenv,subst);
       pages <- 0;
@@ -808,7 +808,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
           self#render_page status ~page ~goal_switch))
 
     method private render_page:
-     'status. #LexiconTypes.status as 'status -> page:int ->
+     'status. #ApplyTransformation.status as 'status -> page:int ->
        goal_switch:Stack.switch -> unit
      = fun status ~page ~goal_switch ->
       (match goal_switch with
@@ -825,7 +825,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
         List.assoc goal_switch goal2win ()
       with Not_found -> assert false)
 
-    method goto_sequent: 'status. #LexiconTypes.status as 'status -> int -> unit
+    method goto_sequent: 'status. #ApplyTransformation.status as 'status -> int -> unit
      = fun status goal ->
       let goal_switch, page =
         try