diff options
| author | Pierre-Marie Pédrot | 2017-07-19 14:05:52 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-07-26 15:12:47 +0200 |
| commit | 906b48ff401f22be6059a6cdde8723b858102690 (patch) | |
| tree | 0254ba66d050474ff0507dc0302d1da3b0d40024 /kernel | |
| parent | 665256fec8465ff0adb943063c25f07a6ca54618 (diff) | |
Avoiding a variable shadowing in the kernel.
This ought to ease the understanding of the code.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/term_typing.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index ed53df01f1..43c099712a 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -274,9 +274,9 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry let j = infer env body in let _ = judge_of_cast env j DEFAULTcast tyj in j, uctx - | SideEffects trust -> + | SideEffects mb -> let (body, uctx, signatures) = inline_side_effects env body uctx side_eff in - let valid_signatures = check_signatures trust signatures in + let valid_signatures = check_signatures mb signatures in let env = push_context_set uctx env in let body,env,ectx = skip_trusted_seff valid_signatures body env in let j = infer env body in |