WARNING: partial commit (does not compile)

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

diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml
index f418abe6f8e658dc3b78eadc9610b9ed380a865a..d0710ab4eab82fed8aee63d2b13adeca1441b335 100644 (file)
--- 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. #NCicCoercion.status as 'status -> NCic.metasenv ->
+   'status. #NTermCicContent.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. #NCicCoercion.status as 'status -> NCic.obj -> unit
+   'status. #NTermCicContent.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
@@ -728,7 +728,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
       self#script#setGoal None
 
     method nload_sequents : 'status. #NTacStatus.tac_status as 'status -> unit
-    = fun status ->
+    = fun (status : #NTacStatus.tac_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. #NCicCoercion.status as 'status -> page:int ->
+     'status. #NTermCicContent.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. #NCicCoercion.status as 'status -> int -> unit
+    method goto_sequent: 'status. #NTermCicContent.status as 'status -> int -> unit
      = fun status goal ->
       let goal_switch, page =
         try