X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Fmain%2FDynFlags.hs;h=6ff79243a53b1403243769322a3cc8bc8bf6a759;hp=e2927226c34b6137d843239c49e91b17d9d3d4b2;hb=4564ccb752ff2dd28176ff1b567b8475fdb8b403;hpb=095c02ee7fbadae65d65a78f558147365190c636

diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index e292722..6ff7924 100644
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -190,9 +190,11 @@ data DynFlag
    | Opt_DoCmmLinting
    | Opt_DoAsmLinting
 
-   | Opt_F_coqpass                      -- run the core-to-core   coqPass (does whatever CoqPass.hs says)
+   | 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_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
-   | Opt_D_dump_coqpass                 -- dumps the output of the core-to-core coqPass
 
    | Opt_WarnIsError                    -- -Werror; makes warnings fatal
    | Opt_WarnDuplicateExports
@@ -1334,9 +1336,11 @@ dynamic_flags = [
   , Flag "dfaststring-stats"       (NoArg (setDynFlag Opt_D_faststring_stats))
 
         ------ Coq-in-GHC ---------------------------
-  , Flag "dcoqpass"                (NoArg (setDynFlag Opt_D_coqpass))
-  , Flag "ddump-coqpass"           (NoArg (setDynFlag Opt_D_dump_coqpass))
+  , 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 "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 }))
 
         ------ Machine dependant (-m<blah>) stuff ---------------------------