string_dec and string in Ocaml library

Question

I have file: `String0.ml` extracted from `String.v` (It is from Coq library) `String.ml` : is a string library of Ocaml After extracted my test file from Coq to Ocaml, I want to used `String.ml` in the library of Ocaml, so I write an replace command to replace all `String0` to `String`. The problem is in the file `test.v`, I used one of the definition: ``` Definition beq_string := beq_dec string_dec. ``` function `string_dec` is not occur in the library of Ocaml, but it has in the string library of Coq So I have an error when I compile `test.ml` ``` open String let beq_string = beq_dec string_dec ``` Error: Unbound value string_dec I want to used the string library of Ocaml for all my extraction files. How can I able to compile `string_dec` ?

Accepted Answer

Extract the `string_dec` function as well.

If you're willing to trust the OCaml library a little, you'll get a lot better performance by extracting `beq_string` to use the built-in equality on strings:

```
Extract Constant beq_string => "((=) : string->string->bool)".
```

string_dec and string in Ocaml library

Solution

Problem