aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/printmod.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-11-08 10:20:08 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-11-09 12:39:15 +0100
commitd69e4f55757c9066b0ae600d14ef89de3c8eb07d (patch)
tree1e3cacf04376924517b0b4be2144ca51f6f60f23 /printing/printmod.ml
parent0d81e80a09db7d352408be4dfc5ba263f6ed98ef (diff)
ssr: fill_occ_pattern: return valid ustate even if no match (fix #6106)
Diffstat (limited to 'printing/printmod.ml')
0 files changed, 0 insertions, 0 deletions