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.

---
 kernel/nativecode.ml   | 2 ++
 kernel/nativelambda.ml | 3 +++
 kernel/nativevalues.ml | 3 ++-
 3 files changed, 7 insertions(+), 1 deletion(-)

(limited to 'kernel')

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
-- 
cgit v1.2.3