diff options
Diffstat (limited to 'doc/RecTutorial/coqartmacros.tex')
| -rw-r--r-- | doc/RecTutorial/coqartmacros.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/RecTutorial/coqartmacros.tex b/doc/RecTutorial/coqartmacros.tex index 6fb7534d53..2a2c211963 100644 --- a/doc/RecTutorial/coqartmacros.tex +++ b/doc/RecTutorial/coqartmacros.tex @@ -46,8 +46,8 @@ \renewcommand{\marginpar}[1]{} \addtocounter{secnumdepth}{1} -\providecommand{\og}{«} -\providecommand{\fg}{»} +\providecommand{\og}{«} +\providecommand{\fg}{»} \newcommand{\hard}{\mbox{\small *}} |