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/mod_subst.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'kernel/mod_subst.ml')

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index f1d08ef6dd..bff3092655 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -319,12 +319,12 @@ let subst_con sub cst =
 let subst_con_kn sub con =
   subst_con sub (con,Univ.Instance.empty)
 
-let subst_pcon sub (con,u as pcon) = 
-  try let con', can = subst_con0 sub pcon in 
+let subst_pcon sub (_con,u as pcon) =
+  try let con', _can = subst_con0 sub pcon in
 	con',u
   with No_subst -> pcon
 
-let subst_pcon_term sub (con,u as pcon) = 
+let subst_pcon_term sub (_con,u as pcon) =
   try let con', can = subst_con0 sub pcon in 
 	(con',u), can
   with No_subst -> pcon, mkConstU pcon
@@ -441,7 +441,7 @@ let replace_mp_in_kn mpfrom mpto kn =
 let rec mp_in_mp mp mp1 =
   match mp1 with
     | _ when ModPath.equal mp1 mp -> true
-    | MPdot (mp2,l) -> mp_in_mp mp mp2
+    | MPdot (mp2,_l) -> mp_in_mp mp mp2
     | _ -> false
 
 let subset_prefixed_by mp resolver =
-- 
cgit v1.2.3