diff options
Diffstat (limited to 'plugins/extraction/common.ml')
| -rw-r--r-- | plugins/extraction/common.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 35d7ba3d5..61e2f8c28 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -45,8 +45,6 @@ let fnl2 () = fnl () ++ fnl () let space_if = function true -> str " " | false -> mt () -let sec_space_if = function true -> spc () | false -> mt () - let is_digit = function | '0'..'9' -> true | _ -> false |