diff options
| author |  Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-21 19:25:49 +0200 |
|---|---|---|
| committer | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-27 21:32:00 +0200 |
| commit | 34d8de84ceb853c98bc80a0623f9afeae317d75f (patch) | |
| tree | e6b4669c12a95297c6abb24c094f430c3fa89432 /kernel | |
| parent | cc12397b32785b06ed892e8ad420cfe253842141 (diff) | |
Locally disable some warnings.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/nativecode.ml | 2 | ||||
| -rw-r--r-- | kernel/nativelambda.ml | 3 | ||||
| -rw-r--r-- | kernel/nativevalues.ml | 3 |
3 files changed, 7 insertions, 1 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index d9659d681..ba80ff590 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 366f9a0a6..fcb75c661 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 965ed67b0..8d5f6388c 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 |