| Opt_DoCmmLinting
| Opt_DoAsmLinting
- | Opt_F_coqpass -- run the core-to-core coqPass (does whatever CoqPass.hs says)
+ | Opt_F_coqpass -- run the core-to-core coqPass, but don't change anything (just "parse/unparse")
+ | Opt_F_skolemize -- run the core-to-core coqPass, skolemizing the proof
+ | Opt_F_flatten -- run the core-to-core coqPass, flattening the proof
+ | Opt_F_simpleopt_before_flatten -- run the "simplPgmOpt" before the coqPass
+ | Opt_D_dump_proofs -- dump natural deduction typing proof of the coqpass input
| Opt_D_coqpass -- run the core-to-string coqPass and dumps the result
- | Opt_D_dump_coqpass -- dumps the output of the core-to-core coqPass
| Opt_WarnIsError -- -Werror; makes warnings fatal
| Opt_WarnDuplicateExports
, Flag "dfaststring-stats" (NoArg (setDynFlag Opt_D_faststring_stats))
------ Coq-in-GHC ---------------------------
- , Flag "dcoqpass" (NoArg (setDynFlag Opt_D_coqpass))
- , Flag "ddump-coqpass" (NoArg (setDynFlag Opt_D_dump_coqpass))
+ , Flag "ddump-proofs" (NoArg (setDynFlag Opt_D_dump_proofs))
+ , Flag "ddump-coqpass" (NoArg (setDynFlag Opt_D_coqpass))
, Flag "fcoqpass" (NoArg (setDynFlag Opt_F_coqpass))
+ , Flag "fsimpleopt-before-flatten" (NoArg (setDynFlag Opt_F_simpleopt_before_flatten))
+ , Flag "fflatten" (NoArg (do { setDynFlag Opt_F_coqpass ; setDynFlag Opt_F_flatten }))
+ , Flag "funsafe-skolemize" (NoArg (do { setDynFlag Opt_F_coqpass ; setDynFlag Opt_F_flatten ; setDynFlag Opt_F_skolemize }))
------ Machine dependant (-m<blah>) stuff ---------------------------