From a3070010c19ec8f46b247875e3c771e2de71dcdf Mon Sep 17 00:00:00 2001
From: Xavier Leroy
Date: Sun, 8 Dec 2019 19:02:51 +0100
Subject: Typo in comment

---
 plugins/extraction/common.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'plugins/extraction/common.ml')

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
-- 
cgit v1.2.3