; ds_binds <- if dopt Opt_F_coqpass dflags
then do { us <- mkSplitUniqSupply '~'
+ ; let do_flatten = dopt Opt_F_flatten dflags
+ ; let do_skolemize = dopt Opt_F_skolemize dflags
; return (coqPassCoreToCore
+ do_flatten
+ do_skolemize
hetmet_brak
hetmet_esc
hetmet_flatten
-- The simpleOptPgm gets rid of type
-- bindings plus any stupid dead code
- ; dumpIfSet_dyn dflags Opt_D_coqpass "Coq Pass Output" $ text $ coqPassCoreToString ds_binds'
+ ; dumpIfSet_dyn dflags Opt_D_dump_proofs "Coq Pass Output" $ text $ coqPassCoreToString ds_binds'
- ; dumpIfSet_dyn dflags Opt_D_dump_coqpass "After Coq Pass" (text $ showSDoc $ pprCoreBindings ds_binds')
+ ; dumpIfSet_dyn dflags Opt_D_coqpass "After Coq Pass" (text $ showSDoc $ pprCoreBindings ds_binds')
; endPass dflags CoreDesugar ds_binds' ds_rules_for_imps