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 ?

Answer 1

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)".