diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-08-12 12:58:58 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-08-12 12:58:58 +0000 |
| commit | 7ba5db11d6e9704d3acb89ca1dbb7cd9890a4385 (patch) | |
| tree | d1af2a89262cbcf5700c6b83bfd968f50179a2ad /interp | |
| parent | aed209d2a59ee71f3f4a434e8c6a6166d48f2eee (diff) | |
Bug et améliorations diverses
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4264 85f007b7-540e-0410-9357-904b9bb8a0f7
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 29f3c437c..97e9855de 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 = |