remove compilation warnings

dune

@@ -2,7 +2,7 @@
  (public_name hol2dk)
  (name main)
  (libraries str unix)
- (flags -w -27 -w -8))
+)
 
 (install
  (files coq.v _CoqProject lambdapi.pkg theory_hol.dk theory_hol.lp encoding.lp renaming.lp erasing.lp fusion.ml bool.ml equal.ml xnames.ml patch unpatch add-links)

fusion.ml

@@ -1,4 +1,5 @@
 (* Slight modification of fusion.ml to dump proofs. *)
+(*REMOVE*)module [@warning "-8-32-27"] M = struct
 
 (* ========================================================================= *)
 (* Complete HOL kernel of types, terms and theorems.                         *)
@@ -937,3 +938,5 @@ let aconv s t = alphaorder s t = 0;;
 (* ------------------------------------------------------------------------- *)
 
 let equals_thm th th' = dest_thm th = dest_thm th';;
+
+(*REMOVE*)end include M

lib.ml

@@ -1,4 +1,5 @@
 (* Slight modification of lib.ml. *)
+module [@warning "-27-39"] M = struct
 
 (* ========================================================================= *)
 (* Convenient library functions.                                             *)
@@ -86,7 +87,7 @@ let rec map2 f l1 l2 =
 (* Attempting function or predicate applications.                            *)
 (* ------------------------------------------------------------------------- *)
 
-let can f x = try (f x; true) with Failure _ -> false;;
+let can f x = try (ignore(f x); true) with Failure _ -> false;;
 
 let check p x = if p x then x else failwith "check";;
 
@@ -847,3 +848,6 @@ let string_of_file filename =
 let file_of_string filename s =
   let fd = Stdlib.open_out filename in
   output_string fd s; close_out fd;;
+
+end
+include M

xdk.ml

@@ -533,7 +533,7 @@ let proof tvs rmap =
 (****************************************************************************)
 
 let typ_arity oc k =
-  for i = 1 to k do out oc "%a -> " typ_name "Set" done; typ_name oc "Set";;
+  for _ = 1 to k do out oc "%a -> " typ_name "Set" done; typ_name oc "Set";;
 
 let decl_typ oc (n,k) =
   out oc "%a : %a.\n" typ_name n typ_arity k;;
@@ -588,7 +588,7 @@ type decl =
 (* [decl_theorem oc k p d] outputs on [oc] the theorem of index [k],
    proof [p] and name [n] as declaration type [d]. *)
 let decl_theorem oc k p d =
-  let Proof(thm,content) = p in
+  let Proof(thm,_) = p in
   (*incr counter;
   if !counter = 1000 then (log "theorem %d ...\n%!" k; counter := 0);*)
   let ts,t = dest_thm thm in

xfiles.ml

@@ -1,6 +1,5 @@
 open Xprelude;;
 open Xlib;;
-open Xnames;;
 
 (* [files()] computes the list of HOL-Light files in the current
    directory and its subdirectories recursively. *)

xlib.ml

@@ -211,7 +211,7 @@ let typ_vars_pos b =
     match l with
     | [] -> acc
     | (Tyvar n, p)::l -> aux ((n, List.rev p)::acc) l
-    | (Tyapp(n,bs), p)::l ->
+    | (Tyapp(_,bs), p)::l ->
        aux acc
          (let k = ref (-1) in
           List.fold_left

xlp.ml

@@ -244,7 +244,7 @@ let abbrev_term =
    constant [el]. *)
 let rec rename rmap t =
   match t with
-  | Var(n,b) -> (try mk_var(List.assoc t rmap,b) with Not_found -> mk_el b)
+  | Var(_,b) -> (try mk_var(List.assoc t rmap,b) with Not_found -> mk_el b)
   | Const(_,_) -> t
   | Comb(u,v) -> mk_comb(rename rmap u, rename rmap v)
   | Abs(u,v) ->
@@ -333,7 +333,7 @@ let subproof tvs rmap ty_su tm_su ts1 i2 oc p2 =
    with type variables [tvs] and free variables renaming map [rmap]. *)
 let proof tvs rmap =
   let term = term rmap in
-  let rec proof oc p =
+  let proof oc p =
     let Proof(thm,content) = p in
     let ts = hyp thm in
     let sub = subproof tvs rmap [] [] ts in
@@ -408,7 +408,7 @@ let proof tvs rmap =
 (* Translation of type declarations and axioms. *)
 (****************************************************************************)
 
-let typ_arity oc k = for i = 1 to k do out oc "Set → " done; out oc "Set";;
+let typ_arity oc k = for _ = 1 to k do out oc "Set → " done; out oc "Set";;
 
 let decl_typ oc (n,k) =
   out oc "constant symbol %a : %a;\n" typ_name n typ_arity k;;
@@ -482,7 +482,7 @@ type decl =
 (* [decl_theorem oc k p d] outputs on [oc] the theorem of index [k]
    and proof [p] as declaration type [d]. *)
 let decl_theorem oc k p d =
-  let Proof(thm,content) = p in
+  let Proof(thm,_) = p in
   (*log "theorem %d ...\n%!" k;*)
   let ts,t = dest_thm thm in
   let xs = freesl (t::ts) in

xnames.ml

@@ -21,7 +21,7 @@ let string_of_file f =
 REMOVE*)
 
 (* [eval code] evaluates [code] in the OCaml toplevel. *)
-let eval (code : string) : unit =
+let [@warning "-27"] eval (code : string) : unit =
   () (*REMOVE
   let as_buf = Lexing.from_string code in
   let parsed = !Toploop.parse_toplevel_phrase as_buf in
@@ -77,7 +77,7 @@ let thms_of_file =
         let _ = Str.search_forward re content start in
         let matches = [Str.matched_group 2 content] in
         search (matches @ acc) (Str.match_end())
-      with e -> (acc)
+      with _ -> acc
     in
     search [] 0
   in
@@ -99,7 +99,7 @@ let thms_of_file =
           [Str.matched_group 2 content
           ;Str.matched_group 3 content] in
         search (matches @ acc) (Str.match_end())
-      with e -> acc
+      with _ -> acc
     in search [] 0
   in
   let search_3 =
@@ -122,7 +122,7 @@ let thms_of_file =
           ;Str.matched_group 4 content]
         in
         search (matches @ acc) (Str.match_end())
-      with e -> acc
+      with _ -> acc
     in search [] 0
   in
   fun f -> let s = string_of_file f in search_1 s @ search_2 s @ search_3 s