diff options
| author | Xavier Leroy | 2019-12-08 19:02:51 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2020-01-08 15:07:16 +0100 |
| commit | a3070010c19ec8f46b247875e3c771e2de71dcdf (patch) | |
| tree | 2cf7018e9b87c8ebce5887418127cb440583bd41 /plugins/extraction | |
| parent | 887128c20edcc7d9a0e6d7387291fe0ba05a29e5 (diff) | |
Typo in comment
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 |