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/declareops.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'kernel/declareops.ml')

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 51ec3defb3..d995786d97 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -181,7 +181,7 @@ let subst_regular_ind_arity sub s =
     if uar' == s.mind_user_arity then s 
     else { mind_user_arity = uar'; mind_sort = s.mind_sort }
 
-let subst_template_ind_arity sub s = s
+let subst_template_ind_arity _sub s = s
 
 (* FIXME records *)
 let subst_ind_arity =
@@ -240,14 +240,14 @@ let inductive_polymorphic_context mib =
 let inductive_is_polymorphic mib =
   match mib.mind_universes with
   | Monomorphic_ind _ -> false
-  | Polymorphic_ind ctx -> true
-  | Cumulative_ind cumi -> true
+  | Polymorphic_ind _ctx -> true
+  | Cumulative_ind _cumi -> true
 
 let inductive_is_cumulative mib =
   match mib.mind_universes with
   | Monomorphic_ind _ -> false
-  | Polymorphic_ind ctx -> false
-  | Cumulative_ind cumi -> true
+  | Polymorphic_ind _ctx -> false
+  | Cumulative_ind _cumi -> true
 
 let inductive_make_projection ind mib ~proj_arg =
   match mib.mind_record with
-- 
cgit v1.2.3