var ddotsub_8f =
[
    [ "ddotsub", "d5/d7e/ddotsub_8f_a7208941a8eaed547ef960320234d20b2.html#a7208941a8eaed547ef960320234d20b2", null ]
];
.