add -fflatten and -funsafe-skolemize flags

[ghc-hetmet.git] / compiler / deSugar / Desugar.lhs

diff --git a/compiler/deSugar/Desugar.lhs b/compiler/deSugar/Desugar.lhs
index 374c13b..f219c01 100644 (file)
--- a/compiler/deSugar/Desugar.lhs
+++ b/compiler/deSugar/Desugar.lhs
@@ -248,7 +248,11 @@ deSugar hsc_env
 
         ; 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
@@ -284,9 +288,9 @@ deSugar hsc_env
                         -- 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