The Coq mailing list

[Keiko Nakata <keiko.nakata AT FireEye.com>]

Hi,

>I have a problem in realising axioms inside functors.
>"Extract Constant" is ignored when inside a functor.
>
>---
>
>  Module N (X:A).
>    Parameter n : bool.
>    (* Does not work *)
>    Extract Constant n => "true".
>  End N.
>
>  Module A_1.
>    Definition a := true.
>  End A_1.
>
>  Module NA_1 := N A_1.
>
>  (* Does not work either *)
>  Extract Constant NA_1.n => "true".
>
>---

The definition of Module Type A was missing.

---

Module Type A.
  Parameter a : bool.
End A.

---

The output of 'Extraction Library' gives

---

open Datatypes

module type A =
  sig
    val a : bool
  end

module N =
  functor (X:A) ->
  struct
    (** val n : bool **)

    let n =
      failwith "AXIOM TO BE REALIZED"
  end

module A_1 =
  struct
    (** val a : bool **)

    let a =
      Coq_true
  end

module NA_1 = N(A_1)

---

where 'Extract Constant' is simply ignored.



Best regards,
Keiko

This email and any attachments thereto may contain private, confidential, 
and/or privileged material for the sole use of the intended recipient. Any 
review, copying, or distribution of this email (or any attachments thereto) 
by others is strictly prohibited. If you are not the intended recipient, 
please contact the sender immediately and permanently delete the original and 
any copies of this email and any attachments thereto.