The Coq mailing list

[Le Xuan Bach <bachdylan AT gmail.com>]

Hi Sir/Madam,

I encounter a problem when extracting my Coq project to Ocaml. Here I will try to replicate the bug in it simplest form.

This is the Coq file:

Module Type A.

End A.

Module A_instance : A.

End A_instance.

Module Type B.

End B.

Module Type C (b : B).

 Declare Module a : A.

End C.

Module Example (a' : A) (b' : B) (c' : C b' with Module a := A_instance).

End Example.

Extraction Language Ocaml.

Set Extraction AutoInline.

Require Import ExtrOcamlBasic.

Require Import ExtrOcamlString.

Extraction "bug.ml" Example.

This is the extracted file:

module type A = 

 sig 

  

 end

module type B = 

 sig 

  

 end

module Example = 

 functor (Coq_a':A) ->

 functor (Coq_b':B) ->

 functor (Coq_c':sig 

  module Coq_a : 

   A

 end) ->

 struct 

  

 end

As you can see, the module Example in the ml file fails to recognize that Coq_a in the functor Coq_c' should be A_instance. This bug happens every time I try to declare "Module a : A b c... with Module k := k_instance" in the functor declaration. It seems that Coq tries to unfold Module a and assign corresponding arguments from b,c,.. but fails to preserve the information in k_instance.

Regards,

Xuan Bach.