diff --git a/Playground.v b/Playground.v
index ba3cfd2..bba807c 100644
--- a/Playground.v
+++ b/Playground.v
@@ -1,10 +1,10 @@
-From MetaCoq.Template      Require Import Loader Ast.
-From MetaCoq.ErasurePlugin Require Import Erasure Loader.
-From MetaCoq.Utils         Require Import utils.
-From MetaCoq.Erasure.Typed Require Import ResultMonad.
-From MetaCoq.Erasure.Typed Require Import Optimize.
-From MetaCoq.Erasure.Typed Require Import Extraction.
-From Coq Require Import ZArith List String Nat.
+From MetaRocq.Template      Require Import Loader Ast.
+From MetaRocq.ErasurePlugin Require Import Erasure Loader.
+From MetaRocq.Utils         Require Import utils.
+From MetaRocq.Erasure.Typed Require Import ResultMonad.
+From MetaRocq.Erasure.Typed Require Import Optimize.
+From MetaRocq.Erasure.Typed Require Import Extraction.
+From Stdlib Require Import ZArith List String Nat.
 
 Import MCMonadNotation.
 Import ListNotations.
diff --git a/agda2lambox.cabal b/agda2lambox.cabal
index a7a688e..a5ee2b7 100644
--- a/agda2lambox.cabal
+++ b/agda2lambox.cabal
@@ -36,7 +36,7 @@ executable agda2lambox
                        LambdaBox.Type,
                        LambdaBox.Env,
                        LambdaBox,
-                       CodeGen.Coq,
+                       CodeGen.Rocq,
                        CodeGen.SExpr,
                        Paths_agda2lambox
   autogen-modules:     Paths_agda2lambox
diff --git a/src/Agda2Lambox/Compile/Monad.hs b/src/Agda2Lambox/Compile/Monad.hs
index 4658bb6..e47f07c 100644
--- a/src/Agda2Lambox/Compile/Monad.hs
+++ b/src/Agda2Lambox/Compile/Monad.hs
@@ -39,9 +39,7 @@ import Data.Foldable (traverse_)
 
 -- | Compilation Environment
 data CompileEnv = CompileEnv
-  { noBlocks :: Bool
-      -- ^ When set to 'True', constructors take no arguments,
-      -- and regular function application is used instead.
+  {
   }
 
 -- | Backend compilation state.
diff --git a/src/Agda2Lambox/Compile/Utils.hs b/src/Agda2Lambox/Compile/Utils.hs
index 545b8ed..e6bb685 100644
--- a/src/Agda2Lambox/Compile/Utils.hs
+++ b/src/Agda2Lambox/Compile/Utils.hs
@@ -85,13 +85,7 @@ toConApp qn es = do
   ctrs <- liftTCM $ getConstructors dt
   ind  <- liftTCM $ toInductive dt
   let idx = fromMaybe 0 $ qn `elemIndex` ctrs
-
-  -- if the no blocks option is enabled
-  -- no argument is given to LConstruct
-  -- and we instead use regular application
-  nb <- asks noBlocks
-  if nb then pure $ foldl' LBox.LApp (LBox.LConstruct ind idx []) es
-        else pure $ LBox.LConstruct ind idx es
+  pure $ foldl' LBox.LApp (LBox.LConstruct ind idx []) es
 
 
 -- | Class for things that may be considered logical, and thus erased.
diff --git a/src/CodeGen/Coq.hs b/src/CodeGen/Coq.hs
deleted file mode 100644
index 08b09f4..0000000
--- a/src/CodeGen/Coq.hs
+++ /dev/null
@@ -1,229 +0,0 @@
-{-# LANGUAGE FlexibleInstances, FlexibleContexts, OverloadedStrings, DataKinds, MonadComprehensions #-}
--- | Generating Coq code from our LambdaBox AST
-module CodeGen.Coq (prettyCoq) where
-
-import Data.Bifunctor(bimap)
-import Data.List(intercalate)
-import Data.List.NonEmpty qualified as NEL
-
-import Agda.Syntax.Common.Pretty
-import LambdaBox
-import Agda.Utils.Function (applyWhen)
-import Agda2Lambox.Compile.Target
-
-
-class ToCoq t a where
-  pcoq  :: Target t -> a -> Doc
-  pcoqP :: Int -> Target t -> a -> Doc
-  pcoq  = pcoqP 0
-  pcoqP = const pcoq
-  {-# MINIMAL pcoq | pcoqP #-}
-
--- | Shorthand for untyped λ□ pretty-printer.
-upcoq :: ToCoq Untyped a => a -> Doc
-upcoq = pcoq ToUntyped
-
--- | Shorthand for typed λ□ pretty-printer.
-tpcoq :: ToCoq Typed a => a -> Doc
-tpcoq = pcoq ToTyped
-
--- | Pretty-print a Coq-printable term.
-prettyCoq :: ToCoq t a => Target t -> a -> String
-prettyCoq t = render . pcoq t
-
--- | Util to format Coq constructor with the given arguments.
-ctor :: String -> [Doc] -> Doc
-ctor = ctorP 0
-{-# INLINE ctor #-}
-
--- | Util to format Coq constructor with the given arguments (and precedence).
-ctorP :: Int -> String -> [Doc] -> Doc
-ctorP p name []   = text name
-ctorP p name args = applyWhen (p >= 10) parens $ text name <?> fsep args
-
--- | Util to format Coq record value with the given fields.
-record :: [(String, Doc)] -> Doc
-record = enclose
-       . fsep
-       . punctuate semi
-       . map \(k, v) -> hang (text k <+> ":=") 2 v
-  where enclose x = "{|" <+> x <+> "|}"
-
-instance ToCoq t Doc  where pcoq _ d = d
-instance ToCoq t Int  where pcoq _ s = pretty s
-instance ToCoq t Bool where pcoq _ v = if v then "true" else "false"
-
-instance {-# OVERLAPPING #-} ToCoq t String where
-  pcoq _ s = text (show s) <> "%bs"
-  -- NOTE(flupe): "%bs" to make sure that we produce Coq bytestrings
-
-instance ToCoq t a => ToCoq t (Maybe a) where
-  pcoqP p t x = case x of
-    Nothing -> ctorP p "None" []
-    Just y  -> ctorP p "Some" [pcoqP 10 t y]
-
-instance ToCoq t a => ToCoq t [a] where
-  pcoq t xs = brackets $ fsep $ punctuate ";" $ map (pcoq t) xs
-
-instance (ToCoq t a, ToCoq t b) => ToCoq t (a, b) where
-  pcoq t (a, b) = parens $ fsep [pcoq t a <> comma, pcoq t b]
-
-instance ToCoq t Name where
-  pcoq t n = case n of
-    Anon    -> ctor "nAnon"  []
-    Named i -> ctor "nNamed" [pcoq t i]
-
-instance ToCoq t ModPath where
-  pcoqP p t mp = case mp of
-    MPFile dp       -> ctorP p "MPfile"  [pcoqP 10 t dp]
-    MPBound dp id i -> ctorP p "MPbound" [pcoqP 10 t dp, pcoqP 10 t id, pcoqP 10 t i]
-    MPDot mp id     -> ctorP p "MPdot"   [pcoqP 10 t mp, pcoqP 10 t id]
-
-instance ToCoq t KerName where
-  pcoq t KerName{..} = pcoq t (kerModPath, kerName)
-
-instance ToCoq t Inductive where
-  pcoq t Inductive{..} =
-    record [ ("inductive_mind", pcoq t indMInd)
-           , ("inductive_ind",  pcoq t indInd)
-           ]
-
-instance ToCoq t d => ToCoq t (Def d) where
-  pcoq t Def{..} =
-    record [ ("dname", pcoq t dName)
-           , ("dbody", pcoq t dBody)
-           , ("rarg",  pcoq t dArgs)
-           ]
-
-instance ToCoq t Term where
-  pcoqP p t v = case v of
-    LBox                -> ctorP p "tBox"       []
-    LRel k              -> ctorP p "tRel"       [pretty k]
-    LLambda n u         -> ctorP p "tLambda"    [pcoq t n, pcoqP 10 t u]
-    LLetIn n u v        -> ctorP p "tLetIn"     [pcoq t n, pcoqP 10 t u, pcoqP 10 t v]
-    LApp u v            -> ctorP p "tApp"       [pcoqP 10 t u, pcoqP 10 t v]
-    LConst c            -> ctorP p "tConst"     [pcoqP 10 t c]
-    LConstruct ind i es -> ctorP p "tConstruct" [pcoqP 10 t ind, pcoqP 10 t i, pcoqP 10 t es]
-    LCase ind n u bs    -> ctorP p "tCase"      [pcoqP 10 t (ind, n), pcoqP 10 t u, pcoqP 10 t bs]
-    LFix mf i           -> ctorP p "tFix"       [pcoqP 10 t mf, pcoqP 10 t i]
-
-instance ToCoq t Type where
-  pcoqP p t v = case v of
-    TBox      -> ctorP p "TBox"   []
-    TAny      -> ctorP p "TAny"   []
-    TArr a b  -> ctorP p "TArr"   [pcoqP 10 t a, pcoqP 10 t b]
-    TApp a b  -> ctorP p "TApp"   [pcoqP 10 t a, pcoqP 10 t b]
-    TVar k    -> ctorP p "TVar"   [pretty k]
-    TInd ind  -> ctorP p "TInd"   [pcoqP 10 t ind]
-    TConst kn -> ctorP p "TConst" [pcoqP 10 t kn]
-
-instance ToCoq t RecursivityKind where
-  pcoq _ rk = case rk of
-    Finite   -> ctor "Finite"   []
-    CoFinite -> ctor "CoFinite" []
-    BiFinite -> ctor "BiFinite" []
-
-instance ToCoq t AllowedElims where
-  pcoq t ae = case ae of
-    IntoSProp        -> ctor "IntoSProp"        []
-    IntoPropSProp    -> ctor "IntoPropSProp"    []
-    IntoSetPropSProp -> ctor "IntoSetPropSProp" []
-    IntoAny          -> ctor "IntoAny"          []
-
-instance ToCoq t (ConstructorBody t) where
-  pcoq ToUntyped Constructor{..} =
-    record [ ("cstr_name",  upcoq cstrName)
-           , ("cstr_nargs", upcoq cstrArgs)
-           ]
-
-  pcoq ToTyped Constructor{..} =
-    tpcoq ((cstrName, getTyped cstrTypes), cstrArgs)
-
-instance ToCoq t (ProjectionBody t) where
-  pcoq ToUntyped Projection{..} = record [("proj_name",  upcoq projName)]
-  pcoq ToTyped   Projection{..} = tpcoq (projName, getTyped projType)
-
-instance ToCoq t TypeVarInfo where
-  pcoq t TypeVarInfo{..} =
-    record
-      [ ("tvar_name",       pcoq t tvarName)
-      , ("tvar_is_logical", pcoq t tvarIsLogical)
-      , ("tvar_is_arity",   pcoq t tvarIsArity)
-      , ("tvar_is_sort",    pcoq t tvarIsSort)
-      ]
-
-instance ToCoq t (OneInductiveBody t) where
-  pcoq t OneInductive{..} =
-    record $
-      [ ("ind_name",          pcoq t indName)
-      , ("ind_propositional", pcoq t indPropositional)
-      , ("ind_kelim",         pcoq t indKElim)
-      , ("ind_ctors",         pcoq t indCtors)
-      , ("ind_projs",         pcoq t indProjs)
-      ] ++
-      case t of
-        ToUntyped -> []
-        ToTyped   -> [("ind_type_vars", pcoq t $ getTyped indTypeVars)]
-
-instance ToCoq t (MutualInductiveBody t) where
-  pcoq t MutualInductive{..} =
-    record [ ("ind_finite", pcoq t indFinite)
-           , ("ind_npars",  pcoq t indPars)
-           , ("ind_bodies", pcoq t indBodies)
-           ]
-
-instance ToCoq t (ConstantBody t) where
-  pcoqP p t ConstantBody{..} =
-    record $
-      [("cst_body", pcoq t cstBody)] ++
-      case t of
-        ToUntyped -> []
-        ToTyped   -> [("cst_type", pcoq t $ getTyped cstType)]
-
-instance ToCoq t (GlobalDecl t) where
-  pcoqP p t decl = case decl of
-    ConstantDecl  body  -> ctorP p "ConstantDecl"  [pcoqP 10 t body]
-    InductiveDecl minds -> ctorP p "InductiveDecl" [pcoqP 10 t minds]
-    TypeAliasDecl typ   -> ctorP p "TypeAliasDecl" [pcoqP 10 t typ]
-
-instance ToCoq t (GlobalEnv t) where
-  pcoq ToUntyped (GlobalEnv env) = upcoq env
-  pcoq ToTyped   (GlobalEnv env) = tpcoq $ flip map env \(kn, decl) -> ((kn, True), decl)
-
-instance ToCoq t (LBoxModule t) where
-  pcoq ToUntyped LBoxModule{..} = vsep
-    [ vcat
-        [ "From Coq             Require Import List."
-        , "From MetaCoq.Common  Require Import BasicAst Kernames Universes."
-        , "From MetaCoq.Utils   Require Import bytestring."
-        , "From MetaCoq.Erasure Require Import EAst."
-        , "From Agda2Lambox     Require Import CheckWF Eval."
-        , "Import ListNotations."
-        ]
-
-    , hang "Definition env : global_declarations :=" 2 $
-        upcoq lboxEnv <> "."
-
-    , "Compute @check_wf_glob eflags env."
-
-    , vsep $ flip map (zip [1..] $ reverse $ NEL.toList $ getUntyped lboxMain) \(i :: Int, kn) -> 
-        let progname = "prog" <> pretty i in vsep
-        [ hang ("Definition " <> progname <> " : program :=") 2 $
-            upcoq (text "env" :: Doc, LConst kn) 
-            <> "."
-        , "Compute eval_program " <> progname <> "."
-        ]
-    ]
-
-  pcoq ToTyped LBoxModule{..} = vsep
-    [ vcat
-        [ "From Coq             Require Import List."
-        , "From MetaCoq.Common  Require Import BasicAst Kernames Universes."
-        , "From MetaCoq.Utils   Require Import bytestring."
-        , "From MetaCoq.Erasure Require Import EAst ExAst."
-        , "From Agda2Lambox     Require Import CheckWF Eval."
-        , "Import ListNotations."
-        ]
-
-    , hang "Definition env : global_env :=" 2 $ tpcoq lboxEnv <> "."
-    ]
diff --git a/src/CodeGen/Rocq.hs b/src/CodeGen/Rocq.hs
new file mode 100644
index 0000000..156302b
--- /dev/null
+++ b/src/CodeGen/Rocq.hs
@@ -0,0 +1,229 @@
+{-# LANGUAGE FlexibleInstances, FlexibleContexts, OverloadedStrings, DataKinds, MonadComprehensions #-}
+-- | Generating Rocq code from our LambdaBox AST
+module CodeGen.Rocq (prettyRocq) where
+
+import Data.Bifunctor(bimap)
+import Data.List(intercalate)
+import Data.List.NonEmpty qualified as NEL
+
+import Agda.Syntax.Common.Pretty
+import LambdaBox
+import Agda.Utils.Function (applyWhen)
+import Agda2Lambox.Compile.Target
+
+
+class ToRocq t a where
+  procq  :: Target t -> a -> Doc
+  procqP :: Int -> Target t -> a -> Doc
+  procq  = procqP 0
+  procqP = const procq
+  {-# MINIMAL procq | procqP #-}
+
+-- | Shorthand for untyped λ□ pretty-printer.
+uprocq :: ToRocq Untyped a => a -> Doc
+uprocq = procq ToUntyped
+
+-- | Shorthand for typed λ□ pretty-printer.
+tprocq :: ToRocq Typed a => a -> Doc
+tprocq = procq ToTyped
+
+-- | Pretty-print a Rocq-printable term.
+prettyRocq :: ToRocq t a => Target t -> a -> String
+prettyRocq t = render . procq t
+
+-- | Util to format Rocq constructor with the given arguments.
+ctor :: String -> [Doc] -> Doc
+ctor = ctorP 0
+{-# INLINE ctor #-}
+
+-- | Util to format Rocq constructor with the given arguments (and precedence).
+ctorP :: Int -> String -> [Doc] -> Doc
+ctorP p name []   = text name
+ctorP p name args = applyWhen (p >= 10) parens $ text name <?> fsep args
+
+-- | Util to format Rocq record value with the given fields.
+record :: [(String, Doc)] -> Doc
+record = enclose
+       . fsep
+       . punctuate semi
+       . map \(k, v) -> hang (text k <+> ":=") 2 v
+  where enclose x = "{|" <+> x <+> "|}"
+
+instance ToRocq t Doc  where procq _ d = d
+instance ToRocq t Int  where procq _ s = pretty s
+instance ToRocq t Bool where procq _ v = if v then "true" else "false"
+
+instance {-# OVERLAPPING #-} ToRocq t String where
+  procq _ s = text (show s) <> "%bs"
+  -- NOTE(flupe): "%bs" to make sure that we produce Rocq bytestrings
+
+instance ToRocq t a => ToRocq t (Maybe a) where
+  procqP p t x = case x of
+    Nothing -> ctorP p "None" []
+    Just y  -> ctorP p "Some" [procqP 10 t y]
+
+instance ToRocq t a => ToRocq t [a] where
+  procq t xs = brackets $ fsep $ punctuate ";" $ map (procq t) xs
+
+instance (ToRocq t a, ToRocq t b) => ToRocq t (a, b) where
+  procq t (a, b) = parens $ fsep [procq t a <> comma, procq t b]
+
+instance ToRocq t Name where
+  procq t n = case n of
+    Anon    -> ctor "nAnon"  []
+    Named i -> ctor "nNamed" [procq t i]
+
+instance ToRocq t ModPath where
+  procqP p t mp = case mp of
+    MPFile dp       -> ctorP p "MPfile"  [procqP 10 t dp]
+    MPBound dp id i -> ctorP p "MPbound" [procqP 10 t dp, procqP 10 t id, procqP 10 t i]
+    MPDot mp id     -> ctorP p "MPdot"   [procqP 10 t mp, procqP 10 t id]
+
+instance ToRocq t KerName where
+  procq t KerName{..} = procq t (kerModPath, kerName)
+
+instance ToRocq t Inductive where
+  procq t Inductive{..} =
+    record [ ("inductive_mind", procq t indMInd)
+           , ("inductive_ind",  procq t indInd)
+           ]
+
+instance ToRocq t d => ToRocq t (Def d) where
+  procq t Def{..} =
+    record [ ("dname", procq t dName)
+           , ("dbody", procq t dBody)
+           , ("rarg",  procq t dArgs)
+           ]
+
+instance ToRocq t Term where
+  procqP p t v = case v of
+    LBox                -> ctorP p "tBox"       []
+    LRel k              -> ctorP p "tRel"       [pretty k]
+    LLambda n u         -> ctorP p "tLambda"    [procq t n, procqP 10 t u]
+    LLetIn n u v        -> ctorP p "tLetIn"     [procq t n, procqP 10 t u, procqP 10 t v]
+    LApp u v            -> ctorP p "tApp"       [procqP 10 t u, procqP 10 t v]
+    LConst c            -> ctorP p "tConst"     [procqP 10 t c]
+    LConstruct ind i es -> ctorP p "tConstruct" [procqP 10 t ind, procqP 10 t i, procqP 10 t es]
+    LCase ind n u bs    -> ctorP p "tCase"      [procqP 10 t (ind, n), procqP 10 t u, procqP 10 t bs]
+    LFix mf i           -> ctorP p "tFix"       [procqP 10 t mf, procqP 10 t i]
+
+instance ToRocq t Type where
+  procqP p t v = case v of
+    TBox      -> ctorP p "TBox"   []
+    TAny      -> ctorP p "TAny"   []
+    TArr a b  -> ctorP p "TArr"   [procqP 10 t a, procqP 10 t b]
+    TApp a b  -> ctorP p "TApp"   [procqP 10 t a, procqP 10 t b]
+    TVar k    -> ctorP p "TVar"   [pretty k]
+    TInd ind  -> ctorP p "TInd"   [procqP 10 t ind]
+    TConst kn -> ctorP p "TConst" [procqP 10 t kn]
+
+instance ToRocq t RecursivityKind where
+  procq _ rk = case rk of
+    Finite   -> ctor "Finite"   []
+    CoFinite -> ctor "CoFinite" []
+    BiFinite -> ctor "BiFinite" []
+
+instance ToRocq t AllowedElims where
+  procq t ae = case ae of
+    IntoSProp        -> ctor "IntoSProp"        []
+    IntoPropSProp    -> ctor "IntoPropSProp"    []
+    IntoSetPropSProp -> ctor "IntoSetPropSProp" []
+    IntoAny          -> ctor "IntoAny"          []
+
+instance ToRocq t (ConstructorBody t) where
+  procq ToUntyped Constructor{..} =
+    record [ ("cstr_name",  uprocq cstrName)
+           , ("cstr_nargs", uprocq cstrArgs)
+           ]
+
+  procq ToTyped Constructor{..} =
+    tprocq ((cstrName, getTyped cstrTypes), cstrArgs)
+
+instance ToRocq t (ProjectionBody t) where
+  procq ToUntyped Projection{..} = record [("proj_name",  uprocq projName)]
+  procq ToTyped   Projection{..} = tprocq (projName, getTyped projType)
+
+instance ToRocq t TypeVarInfo where
+  procq t TypeVarInfo{..} =
+    record
+      [ ("tvar_name",       procq t tvarName)
+      , ("tvar_is_logical", procq t tvarIsLogical)
+      , ("tvar_is_arity",   procq t tvarIsArity)
+      , ("tvar_is_sort",    procq t tvarIsSort)
+      ]
+
+instance ToRocq t (OneInductiveBody t) where
+  procq t OneInductive{..} =
+    record $
+      [ ("ind_name",          procq t indName)
+      , ("ind_propositional", procq t indPropositional)
+      , ("ind_kelim",         procq t indKElim)
+      , ("ind_ctors",         procq t indCtors)
+      , ("ind_projs",         procq t indProjs)
+      ] ++
+      case t of
+        ToUntyped -> []
+        ToTyped   -> [("ind_type_vars", procq t $ getTyped indTypeVars)]
+
+instance ToRocq t (MutualInductiveBody t) where
+  procq t MutualInductive{..} =
+    record [ ("ind_finite", procq t indFinite)
+           , ("ind_npars",  procq t indPars)
+           , ("ind_bodies", procq t indBodies)
+           ]
+
+instance ToRocq t (ConstantBody t) where
+  procqP p t ConstantBody{..} =
+    record $
+      ("cst_body", procq t cstBody) :
+      case t of
+        ToUntyped -> []
+        ToTyped   -> [("cst_type", procq t $ getTyped cstType)]
+
+instance ToRocq t (GlobalDecl t) where
+  procqP p t decl = case decl of
+    ConstantDecl  body  -> ctorP p "ConstantDecl"  [procqP 10 t body]
+    InductiveDecl minds -> ctorP p "InductiveDecl" [procqP 10 t minds]
+    TypeAliasDecl typ   -> ctorP p "TypeAliasDecl" [procqP 10 t typ]
+
+instance ToRocq t (GlobalEnv t) where
+  procq ToUntyped (GlobalEnv env) = uprocq env
+  procq ToTyped   (GlobalEnv env) = tprocq $ flip map env \(kn, decl) -> ((kn, True), decl)
+
+instance ToRocq t (LBoxModule t) where
+  procq ToUntyped LBoxModule{..} = vsep
+    [ vcat
+        [ "From Stdlib           Require Import List."
+        , "From MetaRocq.Common  Require Import BasicAst Kernames Universes."
+        , "From MetaRocq.Utils   Require Import bytestring."
+        , "From MetaRocq.Erasure Require Import EAst."
+        , "From Agda2Lambox     Require Import CheckWF Eval."
+        , "Import ListNotations."
+        ]
+
+    , hang "Definition env : global_declarations :=" 2 $
+        uprocq lboxEnv <> "."
+
+    , "Compute @check_wf_glob eflags env."
+
+    , vsep $ flip map (zip [1..] $ reverse $ NEL.toList $ getUntyped lboxMain) \(i :: Int, kn) -> 
+        let progname = "prog" <> pretty i in vsep
+        [ hang ("Definition " <> progname <> " : program :=") 2 $
+            uprocq (text "env" :: Doc, LConst kn)
+            <> "."
+        , "Compute eval_program " <> progname <> "."
+        ]
+    ]
+
+  procq ToTyped LBoxModule{..} = vsep
+    [ vcat
+        [ "From Stdlib           Require Import List."
+        , "From MetaRocq.Common  Require Import BasicAst Kernames Universes."
+        , "From MetaRocq.Utils   Require Import bytestring."
+        , "From MetaRocq.Erasure Require Import EAst ExAst."
+        , "From Agda2Lambox      Require Import CheckWF Eval."
+        , "Import ListNotations."
+        ]
+
+    , hang "Definition env : global_env :=" 2 $ tprocq lboxEnv <> "."
+    ]
diff --git a/src/CodeGen/SExpr.hs b/src/CodeGen/SExpr.hs
index 8111764..a6e5748 100644
--- a/src/CodeGen/SExpr.hs
+++ b/src/CodeGen/SExpr.hs
@@ -212,5 +212,6 @@ instance ToSexp t (GlobalEnv t) where
 
 instance ToSexp t (LBoxModule t) where
   toSexp t@ToUntyped LBoxModule{..} =
-    toSexp t (lboxEnv, ctor t "tConst" [S $ NEL.head $ getUntyped lboxMain])
-  toSexp t@ToTyped LBoxModule{..} = toSexp t lboxEnv
+    ctor t "Untyped" [S lboxEnv, S $ Just $ LConst $ NEL.head $ getUntyped lboxMain]
+  toSexp t@ToTyped LBoxModule{..} =
+    ctor t "Typed" [S $ toSexp t lboxEnv, S (Nothing :: Maybe Exp)]
diff --git a/src/LambdaBox/Term.hs b/src/LambdaBox/Term.hs
index 5eacf46..4ccd67f 100644
--- a/src/LambdaBox/Term.hs
+++ b/src/LambdaBox/Term.hs
@@ -95,9 +95,10 @@ instance Pretty Term where
         sep [ ("case<" <> pretty ind <> "," <> pretty n <> ">") <+> pretty t <+> "of"
             , nest 2 $ vcat (map (\(n, e) -> sep ["λ<" <> pretty n <> ">", nest 2 (pretty e)]) bs) ]
 
-      LFix ds i -> -- FIXME: for mutual recursion
+      LFix ds i ->
         mparens (p > 0) $
-        hang "μ rec ->" 2 $ pretty $ ds !! i
+        hang ("μrec [" <> pretty i <> "] :=") 2 $
+          vcat (zipWith (\i c -> pretty i <> ": " <> pretty c) ([0..] :: [Int]) ds)
 
       LPrim p -> pretty p
         
diff --git a/src/Main.hs b/src/Main.hs
index 1f3e3af..9e7d757 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -32,7 +32,7 @@ import Agda.Utils ( pp, hasPragma )
 import Agda2Lambox.Compile.Target
 import Agda2Lambox.Compile.Utils
 import Agda2Lambox.Compile ( compile )
-import CodeGen.Coq ( prettyCoq  )
+import CodeGen.Rocq ( prettyRocq  )
 import CodeGen.SExpr ( prettySexp )
 import LambdaBox.Env
 import LambdaBox.Names ( KerName )
@@ -50,11 +50,10 @@ data Options = forall t. Options
   { optOutDir   :: Maybe FilePath
   , optTarget   :: Target t
   , optOutputs  :: [Output]
-  , optNoBlocks :: Bool
   }
 
 instance NFData Options where
-  rnf (Options m t o nb) = rnf m `seq` rnf t `seq` rnf o `seq` rnf nb
+  rnf (Options m t o) = rnf m `seq` rnf t `seq` rnf o
 
 -- | Setter for output directory option.
 outdirOpt :: Monad m => FilePath -> Options -> m Options
@@ -66,16 +65,12 @@ typedOpt opts = return opts { optTarget = ToTyped }
 rocqOpt :: Monad m => Options -> m Options
 rocqOpt opts = return opts { optOutputs = RocqOutput : optOutputs opts }
 
-noBlocksOpt :: Monad m => Options -> m Options
-noBlocksOpt opts = return opts { optNoBlocks = True }
-
 -- | Default backend options.
 defaultOptions :: Options
 defaultOptions  = Options
   { optOutDir   = Nothing
   , optTarget   = ToUntyped
   , optOutputs  = [AstOutput]
-  , optNoBlocks = False
   }
 
 -- | Backend module environments.
@@ -100,8 +95,6 @@ agda2lambox = Backend backend
             "Compile to typed λ□ environments."
           , Option ['c'] ["rocq"] (NoArg rocqOpt)
             "Output a Rocq file."
-          , Option [] ["no-blocks"] (NoArg noBlocksOpt)
-            "Disable constructors as blocks."
           ]
       , isEnabled             = \ _ -> True
       , preCompile            = return
@@ -133,7 +126,7 @@ writeModule Options{..} menv IsMain m defs = do
   -- get defs annotated with a COMPILE pragma
   -- throw an error if none, when targetting untyped lbox
   mains    <- getMain optTarget programs
-  env      <- runCompile (CompileEnv optNoBlocks) $ compile optTarget defs
+  env      <- runCompile CompileEnv $ compile optTarget defs
 
   liftIO $ createDirectoryIfMissing True outDir
 
@@ -151,7 +144,7 @@ writeModule Options{..} menv IsMain m defs = do
 
   when (RocqOutput `elem` optOutputs) $ liftIO $ do
     putStrLn $ "Writing " <> fileName -<.> ".v"
-    prettyCoq optTarget lboxMod <> "\n"
+    prettyRocq optTarget lboxMod <> "\n"
       & writeFile (fileName -<.> ".v")
 
   where
diff --git a/theories/CheckWF.v b/theories/CheckWF.v
index f62482a..8b55230 100644
--- a/theories/CheckWF.v
+++ b/theories/CheckWF.v
@@ -1,8 +1,8 @@
-From Coq             Require Import List Logic.Decidable ssreflect.
-From MetaCoq.Common  Require Import BasicAst Kernames Universes EnvMap.
-From MetaCoq.Erasure Require Import EAst EWellformed.
-From MetaCoq.Utils   Require Import bytestring ReflectEq.
-From Equations       Require Import Equations.
+From Stdlib           Require Import List Logic.Decidable ssreflect.
+From MetaRocq.Common  Require Import BasicAst Kernames Universes EnvMap.
+From MetaRocq.Erasure Require Import EAst EWellformed.
+From MetaRocq.Utils   Require Import bytestring ReflectEq.
+From Equations        Require Import Equations.
 
 Import ListNotations.
 Import EnvMap.
diff --git a/theories/Eval.v b/theories/Eval.v
index 3049edf..5372053 100644
--- a/theories/Eval.v
+++ b/theories/Eval.v
@@ -1,8 +1,8 @@
 (* This file provides utilises to evaluate lambda box programs *)
 
-From Coq                   Require Import Nat.
-From MetaCoq.Utils         Require Import utils.
-From MetaCoq.Erasure       Require Import EAst.
+From Stdlib                Require Import Nat.
+From MetaRocq.Utils        Require Import utils.
+From MetaRocq.Erasure      Require Import EAst.
 From CertiCoq.Common       Require Import Common.
 From CertiCoq.LambdaBoxMut Require Import compile term program wcbvEval.