1 2 3 4 5 6 7
(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-extraction-logical-axiom") -*- *) Require Extraction. Axiom foo : Prop. Extraction foo.