The Coq mailing list

[Jianzhou Zhao <jianzhou AT seas.upenn.edu>]

Hi,

In 8.2 I was extracting code from Modules. For example:

(* start  test.v *)
Module A.
  Definition INT:=nat.
  Definition test (i:INT) := i.
End A.

Extract Constant A.INT => "int".
Extraction "test" A.test.
(* end  test.v *)

"coqc test.v" generates "test.mli" and "test.ml" as the below.

(* start test.mli *)
type nat =
  | O
  | S of nat

module A :
 sig
  type coq_INT = nat
  val test : coq_INT -> coq_INT
 end
(* end test.mli *)

(* start test.ml *)
type nat =
  | O
  | S of nat

module A =
 struct
  type coq_INT = int

  (** val test : coq_INT -> coq_INT **)
  let test i =
    i
 end
(* end test.ml *)

OCaml cannot compile them because A.coq_INT in test.ml does not match
A.coq_INT in test.mli. Extract Constant A.INT => "int" does not change
A.coq_INT in the module signature. Is this the correct way to do
extractions from modules?

Thanks
-- 
Jianzhou