Rename to MetaRocq

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.

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

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.

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.