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/cooking.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/cooking.ml')

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 657478a106..b361e36bbf 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -91,7 +91,7 @@ let update_case_info cache ci modlist =
   try
     let ind, n =
       match share cache (IndRef ci.ci_ind) modlist with
-      | (IndRef f,(u,l)) -> (f, Array.length l)
+      | (IndRef f,(_u,l)) -> (f, Array.length l)
       | _ -> assert false in
     { ci with ci_ind = ind; ci_npar = ci.ci_npar + n }
   with Not_found ->
-- 
cgit v1.2.3