The Coq mailing list

["Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>]

Ah, nice idea!

On May 31, 2017, at 8:21 AM, Matthieu Sozeau <mattam AT mattam.org> wrote:

I guess you could use an extraction directive to extract foo to [Obj.magic ()] to avoid this.

On Mon, May 29, 2017 at 4:21 PM Benjamin C. Pierce <bcpierce AT cis.upenn.edu> wrote:

I’d like to be able to extract an ML program from a Coq file that is missing some definitions.  For example, suppose I have a file temp.v containing

Definition foo (x:nat) : bool. Admitted.

Definition bar (x:nat) : bool := true.

and I want to play with bar before finishing foo.  If I do

Require Import temp.

Extraction Library temp.

what I get in temp.ml is

open Datatypes

(** val foo : nat -> bool **)

let foo =

  failwith "AXIOM TO BE REALIZED"

(** val bar : nat -> bool **)

let bar _ =

  Coq_true

which is not helpful (executing this code simply raises an error, whether or not foo is called).  

Is there a better way?

Thanks!

      - Benjamin