title: OCaml string and Coq string (Extraction from Coq to OCaml)
body: <p>I used the extraction from Coq to OCaml, where I have type <code>Z</code>, <code>N</code>, <code>positive</code></p>
  
  <p>I don't use to extract it in <code>int</code> of OCaml.</p>
  
  <p>Then the type I have after the extraction is:</p>
  
  <pre><code>type positive =
  | Coq_xI of positive
  | Coq_xO of positive
  | Coq_xH
  
  type coq_N =
  | N0
  | Npos of positive
  
  type coq_Z =
  | Z0
  | Zpos of positive
  | Zneg of positive
  </code></pre>
  
  <p>I have a program in OCaml where some functions using the OCaml type <code>string</code>.</p>
  
  <p>In my OCaml program, I need to write some functions convert the type: <code>string -&gt; coq_N</code>, <code>string -&gt; coq_Z</code>, <code>string -&gt; positive</code></p>
  
  <p>I tried to write the functions in Coq and then used the extraction to get the OCaml type but Coq <code>string</code> is different from OCaml <code>string</code>.</p>
  
  <p>For instance:</p>
  
  <pre><code>open Ascii
  open BinNums
  open Datatypes
  
  type string =
  | EmptyString
  | String of ascii * string
  
  let string_of_coqN (s: string): coq_N =
    match s with
      | EmptyString -&gt; N0
      | String (a, _) -&gt; (coq_N_of_ascii a);;
  </code></pre>
  
  <p>where <code>coq_N_of_ascii</code> is the extraction from <code>coq</code> function <code>N_of_ascii</code>.</p>
  
  <p>When I applied the function <code>string_of_coqN</code>, for instance:</p>
  
  <pre><code>let test (x: string) = string_of_N x;;
  </code></pre>
  
  <p>I got the complain that </p>
  
  <pre><code>Error: This expression has type string but an expression was expected of type
           String0.string
  </code></pre>
  
  <p>Could you please help me to find a way to write the convert functions : <code>string -&gt; coq_N</code>, <code>string -&gt; coq_Z</code> and <code>string -&gt; positive</code>?</p>