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

(limited to 'kernel/context.ml')

diff --git a/kernel/context.ml b/kernel/context.ml
index 4a7204b75c..3d98381fbb 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -142,8 +142,8 @@ struct
     (** Reduce all terms in a given declaration to a single value. *)
     let fold_constr f decl acc =
       match decl with
-      | LocalAssum (n,ty) -> f ty acc
-      | LocalDef (n,v,ty) -> f ty (f v acc)
+      | LocalAssum (_n,ty) -> f ty acc
+      | LocalDef (_n,v,ty) -> f ty (f v acc)
 
     let to_tuple = function
       | LocalAssum (na, ty) -> na, None, ty
@@ -151,7 +151,7 @@ struct
 
     let drop_body = function
       | LocalAssum _ as d -> d
-      | LocalDef (na, v, ty) -> LocalAssum (na, ty)
+      | LocalDef (na, _v, ty) -> LocalAssum (na, ty)
 
   end
 
@@ -356,7 +356,7 @@ struct
 
     let drop_body = function
       | LocalAssum _ as d -> d
-      | LocalDef (id, v, ty) -> LocalAssum (id, ty)
+      | LocalDef (id, _v, ty) -> LocalAssum (id, ty)
 
     let of_rel_decl f = function
       | Rel.Declaration.LocalAssum (na,t) ->
-- 
cgit v1.2.3