X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaMathView.ml;h=271a7b19ab45c664f61aac4c805b435d81415044;hb=1aca50505c3ce6c76dd7d20d00e358707caffd4a;hp=ef7780f0c88a8b3993a2c6628007ed1e1d63d5b0;hpb=bd81dfa48a0a2c8c6da42bd62e0357c5ed862179;p=helm.git

diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml
index ef7780f0c..271a7b19a 100644
--- a/matita/matita/matitaMathView.ml
+++ b/matita/matita/matitaMathView.ml
@@ -27,9 +27,7 @@
 
 open Printf
 
-open GrafiteTypes
 open MatitaGtkMisc
-open MatitaGuiTypes
 open CicMathView
 
 module Stack = Continuationals.Stack
@@ -91,7 +89,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
           GtkSignal.disconnect notebook#as_widget id;
           switch_page_callback <- None
       | None -> ());
-      for i = 0 to pages do notebook#remove_page 0 done; 
+      for _i = 0 to pages do notebook#remove_page 0 done; 
       notebook#set_show_tabs true;
       pages <- 0;
       page2goal <- [];
@@ -112,12 +110,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
           scrolledWin <- Some w;
           (match cicMathView#misc#parent with
             | None -> ()
-            | Some parent ->
-               let parent =
-                match cicMathView#misc#parent with
-                   None -> assert false
-                 | Some p -> GContainer.cast_container p
-               in
+            | Some p ->
+               let parent = GContainer.cast_container p in
                 parent#remove cicMathView#coerce);
           w#add cicMathView#coerce
         in
@@ -128,8 +122,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
         let stack_goals = Stack.open_goals status#stack in
         let proof_goals = List.map fst metasenv in
         if
-          HExtlib.list_uniq (List.sort Pervasives.compare stack_goals)
-          <> List.sort Pervasives.compare proof_goals
+          HExtlib.list_uniq (List.sort compare stack_goals)
+          <> List.sort compare proof_goals
         then begin
           prerr_endline ("STACK GOALS = " ^ String.concat " " (List.map string_of_int stack_goals));
           prerr_endline ("PROOF GOALS = " ^ String.concat " " (List.map string_of_int proof_goals));
@@ -158,7 +152,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
       in
       let add_switch _ _ (_, sw) = add_tab (render_switch sw) sw in
       Stack.iter  (** populate notebook with tabs *)
-        ~env:(fun depth tag (pos, sw) ->
+        ~env:(fun depth _tag (pos, sw) ->
           let markup =
             match depth, pos with
             | 0, 0 -> `Current (render_switch sw)
@@ -180,12 +174,12 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
     method private render_page:
      'status. #ApplyTransformation.status as 'status -> page:int ->
        goal_switch:Stack.switch -> unit
-     = fun status ~page ~goal_switch ->
+     = fun status ~page:_ ~goal_switch ->
       (match goal_switch with
       | Stack.Open goal ->
          let menv,subst = _metasenv in
           cicMathView#nload_sequent status menv subst goal
-      | Stack.Closed goal ->
+      | Stack.Closed _goal ->
           let root = Lazy.force closed_goal_mathml in
           cicMathView#load_root ~root);
       (try
@@ -479,7 +473,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       self#_showMath;
       mathView#load_root (Lazy.force empty_mathml)
 
-    method private _loadCheck term =
+    method private _loadCheck _term =
       failwith "not implemented _loadCheck";
 (*       self#_showMath *)
 
@@ -504,7 +498,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
          "the graph of dependencies amoung objects. Please install it.")
         ~parent:win#toplevel ()
 
-    method private dependencies direction uri () =
+    method private dependencies _direction _uri () =
       assert false (* MATITA 1.0
       let dbd = LibraryDb.instance () in
       let graph =
@@ -579,7 +573,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       let content = Http_getter.ls ~local:false dir in
       let l =
         List.fast_sort
-          Pervasives.compare
+          compare
           (List.map
             (function 
               | Http_getter_types.Ls_section s -> "dir", s
@@ -728,7 +722,7 @@ let find_selection_owner () =
     | mv :: tl ->
         (match mv#get_selections with
         | [] -> aux tl
-        | sel :: _ -> mv)
+        | _sel :: _ -> mv)
   in
   aux (get_math_views ())