add -fsimpleopt-before-flatten

[ghc-hetmet.git] / compiler / main / DynFlags.hs

diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index 6ff7924..6fe6708 100644 (file)
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -193,6 +193,7 @@ data DynFlag
    | 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
 
@@ -1339,6 +1340,7 @@ dynamic_flags = [
   , 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 }))