X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2FdeSugar%2FDesugar.lhs;h=f219c019796f0cd52ab11b7f7db237a8f12dd827;hp=374c13b6260cb952872408cf0f9a0834a2ca0699;hb=4564ccb752ff2dd28176ff1b567b8475fdb8b403;hpb=095c02ee7fbadae65d65a78f558147365190c636

diff --git a/compiler/deSugar/Desugar.lhs b/compiler/deSugar/Desugar.lhs
index 374c13b..f219c01 100644
--- 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