aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/declarations.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-14 17:38:55 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-14 17:38:55 +0100
commit71662ab9b00ac657663e192d942a4ba7f241fd59 (patch)
tree3b421d598ff38fc3490c82df9d562ac7ec1bed44 /kernel/declarations.ml
parent0de6c50cb895bce977db0d5c1b603940706ccd03 (diff)
parentd69e4f55757c9066b0ae600d14ef89de3c8eb07d (diff)
Merge PR #6116: ssr: fill_occ_pattern: return valid ustate even if no match (fix #6106)
Diffstat (limited to 'kernel/declarations.ml')
0 files changed, 0 insertions, 0 deletions