diff options
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/common.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index e2cde8e0d3..742dca612a 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -698,9 +698,10 @@ let rec is_native_string_rec empty_string_ref string_constructor_ref = function (* others *) | _ -> false -(* Here we first check that the argument is has a type registered as core.string.type - and that extraction to native strings was requested. - Then we check every character via [is_native_string_rec]. *) +(* Here we first check that the argument is the type registered as + core.string.type and that extraction to native strings was + requested. Then we check every character via + [is_native_string_rec]. *) let is_native_string c = match c with |