From 2cceef0e3cab18b1dcc28bf1c8ce6b4723cd3d9a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 21 May 2018 21:48:00 +0200
Subject: [kernel] Compile with almost all warnings enabled.

This is a partial resurrection of #6423 but only for the kernel.

IMHO, we pay a bit of price for this but it is a good safety
measure.

Only warning "4: fragile pattern matching" and "44: open hides a type"
are disabled.

We would like to enable 44 for sure once we do some alias cleanup.
---
 kernel/nativelib.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel/nativelib.ml')

diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index f784509b6f..b4126dd68c 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -40,7 +40,7 @@ let include_dirs () =
   [Filename.get_temp_dir_name (); coqlib () / "kernel"; coqlib () / "library"]
 
 (* Pointer to the function linking an ML object into coq's toplevel *)
-let load_obj = ref (fun x -> () : string -> unit)
+let load_obj = ref (fun _x -> () : string -> unit)
 
 let rt1 = ref (dummy_value ())
 let rt2 = ref (dummy_value ())
@@ -113,7 +113,7 @@ let call_compiler ?profile:(profile=false) ml_filename =
     let res = CUnix.sys_command (ocamlfind ()) args in
     let res = match res with
       | Unix.WEXITED 0 -> true
-      | Unix.WEXITED n | Unix.WSIGNALED n | Unix.WSTOPPED n ->
+      | Unix.WEXITED _n | Unix.WSIGNALED _n | Unix.WSTOPPED _n ->
         warn_native_compiler_failed (Inl res); false
     in
     res, link_filename
@@ -158,7 +158,7 @@ let call_linker ?(fatal=true) prefix f upds =
   (try
     if Dynlink.is_native then Dynlink.loadfile f else !load_obj f;
     register_native_file prefix
-   with Dynlink.Error e as exn ->
+   with Dynlink.Error _ as exn ->
      let exn = CErrors.push exn in
      if fatal then iraise exn
      else if !Flags.debug then Feedback.msg_debug CErrors.(iprint exn));
-- 
cgit v1.2.3