diff options
| author | Emilio Jesus Gallego Arias | 2018-05-21 21:48:00 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-09-24 15:27:18 +0200 |
| commit | 2cceef0e3cab18b1dcc28bf1c8ce6b4723cd3d9a (patch) | |
| tree | 2b584a747ffca2f18c96a81b2498ef82a3e3348d /kernel/context.ml | |
| parent | c2a1cc7473cf4db27ee47ac011409f7a1839b36d (diff) | |
[kernel] Compile with almost all warnings enabled.
This is a partial resurrection of #6423 but only for the kernel.
IMHO, we pay a bit of price for this but it is a good safety
measure.
Only warning "4: fragile pattern matching" and "44: open hides a type"
are disabled.
We would like to enable 44 for sure once we do some alias cleanup.
Diffstat (limited to 'kernel/context.ml')
| -rw-r--r-- | kernel/context.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/context.ml b/kernel/context.ml index 4a7204b75c..3d98381fbb 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -142,8 +142,8 @@ struct (** Reduce all terms in a given declaration to a single value. *) let fold_constr f decl acc = match decl with - | LocalAssum (n,ty) -> f ty acc - | LocalDef (n,v,ty) -> f ty (f v acc) + | LocalAssum (_n,ty) -> f ty acc + | LocalDef (_n,v,ty) -> f ty (f v acc) let to_tuple = function | LocalAssum (na, ty) -> na, None, ty @@ -151,7 +151,7 @@ struct let drop_body = function | LocalAssum _ as d -> d - | LocalDef (na, v, ty) -> LocalAssum (na, ty) + | LocalDef (na, _v, ty) -> LocalAssum (na, ty) end @@ -356,7 +356,7 @@ struct let drop_body = function | LocalAssum _ as d -> d - | LocalDef (id, v, ty) -> LocalAssum (id, ty) + | LocalDef (id, _v, ty) -> LocalAssum (id, ty) let of_rel_decl f = function | Rel.Declaration.LocalAssum (na,t) -> |