diff options
| author | Emilio Jesus Gallego Arias | 2018-05-21 21:48:00 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-09-24 15:27:18 +0200 |
| commit | 2cceef0e3cab18b1dcc28bf1c8ce6b4723cd3d9a (patch) | |
| tree | 2b584a747ffca2f18c96a81b2498ef82a3e3348d /kernel/nativelib.ml | |
| parent | c2a1cc7473cf4db27ee47ac011409f7a1839b36d (diff) | |
[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.
Diffstat (limited to 'kernel/nativelib.ml')
| -rw-r--r-- | kernel/nativelib.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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)); |