From 34d8de84ceb853c98bc80a0623f9afeae317d75f Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 19:25:49 +0200
Subject: Locally disable some warnings.

---
 checker/declarations.ml | 2 ++
 dev/top_printers.ml     | 1 +
 kernel/nativecode.ml    | 2 ++
 kernel/nativelambda.ml  | 3 +++
 kernel/nativevalues.ml  | 3 ++-
 lib/backtrace.ml        | 1 +
 6 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/checker/declarations.ml b/checker/declarations.ml
index 1fe02c8b60..56d437c165 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -6,6 +6,7 @@ open Term
 (** Substitutions, code imported from kernel/mod_subst *)
 
 module Deltamap = struct
+  [@@@ocaml.warning "-32-34"]
   type t = delta_resolver
   let empty = MPmap.empty, KNmap.empty
   let is_empty (mm, km) = MPmap.is_empty mm && KNmap.is_empty km
@@ -25,6 +26,7 @@ end
 let empty_delta_resolver = Deltamap.empty
 
 module Umap = struct
+  [@@@ocaml.warning "-32-34"]
   type 'a t = 'a umap_t
   let empty = MPmap.empty, MBImap.empty
   let is_empty (m1,m2) = MPmap.is_empty m1 && MBImap.is_empty m2
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 474cc85c17..918e98f778 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 (* Printers for the ocaml toplevel. *)
+[@@@ocaml.warning "-32"]
 
 open Util
 open Pp
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index d9659d6813..ba80ff590d 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -16,6 +16,8 @@ open Nativeinstr
 open Nativelambda
 open Pre_env
 
+[@@@ocaml.warning "-32-37"]
+
 (** This file defines the mllambda code generation phase of the native
 compiler. mllambda represents a fragment of ML, and can easily be printed
 to OCaml code. *)
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 366f9a0a6d..fcb75c661e 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -16,6 +16,9 @@ open Nativeinstr
 
 module RelDecl = Context.Rel.Declaration
 
+(* I'm not messing with this stuff. *)
+[@@@ocaml.warning "-32"]
+
 (** This file defines the lambda code generation phase of the native compiler *)
 
 exception NotClosed
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 965ed67b07..8d5f6388cb 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -334,6 +334,7 @@ let l_or accu x y =
   if is_int x && is_int y then no_check_l_or x y
   else accu x y
 
+[@@@ocaml.warning "-37"]
 type coq_carry = 
   | Caccu of t
   | C0 of t
@@ -430,7 +431,7 @@ let addmuldiv accu x y z =
   if is_int x && is_int y && is_int z then no_check_addmuldiv x y z
   else accu x y z
 
-
+[@@@ocaml.warning "-34"]
 type coq_bool =
   | Baccu of t
   | Btrue
diff --git a/lib/backtrace.ml b/lib/backtrace.ml
index b3b8bdea2e..be9f40c1fb 100644
--- a/lib/backtrace.ml
+++ b/lib/backtrace.ml
@@ -5,6 +5,7 @@
 (*    //   *      This file is distributed under the terms of the      *)
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
+[@@@ocaml.warning "-37"]
 
 type raw_frame =
 | Known_location of bool   (* is_raise *)
-- 
cgit v1.2.3