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/nativevalues.ml | |
| parent | cc12397b32785b06ed892e8ad420cfe253842141 (diff) | |
Locally disable some warnings.
Diffstat (limited to 'kernel/nativevalues.ml')
| -rw-r--r-- | kernel/nativevalues.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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 |