diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/table.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 4322ac95fa..dd3b65b908 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -413,7 +413,7 @@ let msg_non_implicit r n id = | Anonymous -> "" | Name id -> "(" ^ string_of_id id ^ ") " in - "The " ^ (ordinal n) ^ " argument " ^ name ^ "of " ^ (string_of_global r) + "The " ^ (String.ordinal n) ^ " argument " ^ name ^ "of " ^ (string_of_global r) let error_non_implicit msg = err (str (msg ^ " still occurs after extraction.") ++ |