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 /checker | |
| parent | cc12397b32785b06ed892e8ad420cfe253842141 (diff) | |
Locally disable some warnings.
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/declarations.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml index 1fe02c8b6..56d437c16 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 |