aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/assumptions.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-07-19 14:05:52 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-07-26 15:12:47 +0200
commit906b48ff401f22be6059a6cdde8723b858102690 (patch)
tree0254ba66d050474ff0507dc0302d1da3b0d40024 /vernac/assumptions.ml
parent665256fec8465ff0adb943063c25f07a6ca54618 (diff)
Avoiding a variable shadowing in the kernel.
This ought to ease the understanding of the code.
Diffstat (limited to 'vernac/assumptions.ml')
0 files changed, 0 insertions, 0 deletions