-{-
- ; dumpIfSet_dyn dflags Opt_D_dump_proof "input to flattener" (text $ showSDoc $ pprCoreBindings ds_binds)
- ; let uhandler (err::ErrorCall)
- = dumpIfSet_dyn dflags Opt_D_dump_proof "System FC Proof"
- (text $ "\\begin{verbatim}\n" ++
- show err ++
- "\\end{verbatim}\n\n")
- in (dumpIfSet_dyn dflags Opt_D_dump_proof "System FC Proof" $
- (vcat (map (\ bind -> let e = case bind of
- NonRec b e -> e
- Rec lve -> Let (Rec lve) (Var unitDataConId)
- in text $ "\\begin{verbatim}\n" ++
- (showSDoc $ pprCoreBindings ds_binds) ++
- "\\end{verbatim}\n\n" ++
- "$$\n"++
- (core2proofAndShow e) ++
- "$$\n"
- ) ds_binds))) `Control.Exception.catch` uhandler
--}
- ; endPass dflags CoreDesugar ds_binds ds_rules_for_imps
+
+ ; dumpIfSet_dyn dflags Opt_D_coqpass "Coq Pass Output" $ text $ coqPassCoreToString ds_binds
+
+ ; ds_binds' <- if dopt Opt_F_coqpass dflags
+ then return $ coqPassCoreToCore ds_binds
+ else return ds_binds
+
+ ; dumpIfSet_dyn dflags Opt_D_dump_coqpass "After Coq Pass" (text $ showSDoc $ pprCoreBindings ds_binds')
+
+ ; endPass dflags CoreDesugar ds_binds' ds_rules_for_imps