Some why3doc comments in the gallery contains "[i,j[", which breaks the
documentation since it opens a code block that is never closed. The proper
way to write it is "[\[i,j\[]", which is not only ugly but also
error-prone.

This commit introduces a Markdown-like syntax for embedded code. It uses
the backtick as a delimiter: "`[i,j[`". It also supports multi-backticks:
"you can delimit code using `` `...` ``".