Some cleaning.

src/ide/why3ide.ml

@@ -200,14 +200,6 @@ let () =
   Gconfig.init ()
 
 
-
-
-
-
-
-
-
-
 (********************************)
 (* Source language highlighting *)
 (********************************)
@@ -249,10 +241,6 @@ let try_convert s =
     with Glib.Convert.Error _ as e -> Printexc.to_string e
 
 
-
-
-
-
 (****************************)
 (* Color handling in source *)
 (****************************)
@@ -286,10 +274,6 @@ let erase_color_loc (v:GSourceView2.source_view) =
 
 
 
-
-
-
-
 (*******************)
 (* Graphical tools *)
 (*******************)
@@ -375,19 +359,6 @@ let update_label_saved (label: GMisc.label) =
     label#set_text (String.sub s 1 (String.length s - 1))
 
 
-
-
-
-
-
-
-
-
-
-
-
-
-
 (**********************)
 (* Graphical elements *)
 (**********************)

src/transform/case.ml

 open Trans
 open Term
+open Ident
+open Ty
 open Decl
 open Theory
 open Task
@@ -16,7 +18,7 @@ exception Cannot_infer_type of string
 let debug_matching = Debug.register_info_flag "print_match"
   ~desc:"Print@ terms@ that@ were@ not@ successfully@ matched@ by@ ITP@ tactic@ apply."
 
-let rec dup n x = if n = 0 then [] else x::(dup (n-1) x)
+(* let rec dup n x = if n = 0 then [] else x::(dup (n-1) x) *)
 
 let gen_ident = Ident.id_fresh
 
@@ -509,12 +511,6 @@ let or_intro (left: bool) : Task.task Trans.trans =
       end
     | _ -> [d]) None
 
-(* TODO to be done ... *)
-open Ident
-open Ty
-open Term
-open Decl
-
 (* TODO temporary for intros *)
 let rec intros n pr f =
   if n = 0 then [create_prop_decl Pgoal pr f] else
@@ -715,9 +711,9 @@ let () = wrap_and_register
     ~desc:"apply <prop> applies prop to the goal" "apply"
     (Tprsymbol Ttrans_l) apply
 
-let () = wrap_and_register
-    ~desc:"duplicate <int> duplicates the goal int times" "duplicate"
-    (Tint Ttrans_l) (fun x -> Trans.store (dup x))
+(* let () = wrap_and_register *)
+(*     ~desc:"duplicate <int> duplicates the goal int times" "duplicate" *)
+(*     (Tint Ttrans_l) (fun x -> Trans.store (dup x)) *)
 
 let () = wrap_and_register
     ~desc:"use_th <theory> imports the theory" "use_th"