diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 29f3c437c5..97e9855de8 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -125,8 +125,13 @@ let translate_keyword = function | "if" | "then" | "else" | "return" as s) -> let s' = s^"_" in msgerrnl - (str ("Warning: "^s^" is now a keyword; it has been translated to "^s')); + (str ("Warning: '"^ + s^"' is now a keyword; it has been translated to '"^s'^"'")); s' + | "_" -> + msgerrnl (str + "Warning: '_' is no longer a keyword; it has been translated to 'xx'"); + "xx" | s -> s let is_coq_root d = |