diff options
Diffstat (limited to 'parsing/extrawit.ml')
| -rw-r--r-- | parsing/extrawit.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml index be584b5c8..3e1c44e5a 100644 --- a/parsing/extrawit.ml +++ b/parsing/extrawit.ml @@ -49,7 +49,7 @@ let rawwit_tactic = function | n -> Errors.anomaly ("Unavailable tactic level: "^string_of_int n) let tactic_genarg_level s = - if String.length s = 7 && String.sub s 0 6 = "tactic" then + if Int.equal (String.length s) 7 && String.sub s 0 6 = "tactic" then let c = s.[6] in if '5' >= c && c >= '0' then Some (Char.code c - 48) else None else None |