aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 8fd7efd60..4b04f4c9f 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -125,7 +125,7 @@ let raw_string_of_ref = function
let translate_keyword = function
| ("forall" | "fun" | "match" | "fix" | "cofix" | "for" | "let"
- | "if" | "then" | "else" | "return" as s) ->
+ | "if" | "then" | "else" | "return" | "mod" as s) ->
let s' = s^"_" in
msgerrnl
(str ("Warning: '"^