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/vars.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/vars.ml')
| -rw-r--r-- | kernel/vars.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/vars.ml b/kernel/vars.ml index 0f588a6302..9d5d79124b 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -66,7 +66,7 @@ let isMeta c = match Constr.kind c with let noccur_with_meta n m term = let rec occur_rec n c = match Constr.kind c with | Constr.Rel p -> if n<=p && p<n+m then raise LocalOccur - | Constr.App(f,cl) -> + | Constr.App(f,_cl) -> (match Constr.kind f with | Constr.Cast (c,_,_) when isMeta c -> () | Constr.Meta _ -> () @@ -188,7 +188,7 @@ let adjust_rel_to_rel_context sign n = let open RelDecl in match sign with | LocalAssum _ :: sign' -> let (n',p) = aux sign' in (n'+1,p) - | LocalDef (_,c,_)::sign' -> let (n',p) = aux sign' in (n'+1,if n'<n then p+1 else p) + | LocalDef (_,_c,_)::sign' -> let (n',p) = aux sign' in (n'+1,if n'<n then p+1 else p) | [] -> (0,n) in snd (aux sign) |