Module DemoExtract

Require Import DemoHeader DemoTarget.

Extract Inductive list => "list" [ "[]" "(::)" ].
Extract Inlined Constant Datatypes.fst => "fst".
Extract Inlined Constant Datatypes.snd => "snd".
Extract Inductive prod => "