diff options
Diffstat (limited to 'translate/ppvernacnew.ml')
| -rw-r--r-- | translate/ppvernacnew.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index 100ac9d6ca..d8d3493163 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -151,7 +151,7 @@ let pr_production_item = function let pr_comment pr_c = function | CommentConstr c -> pr_c c - | CommentString s -> str s + | CommentString s -> qs s | CommentInt n -> int n let pr_in_out_modules = function |