diff --git a/lib/Parse/PostProcess.ml b/lib/Parse/PostProcess.ml
deleted file mode 100644
index 773ae6a..0000000
--- a/lib/Parse/PostProcess.ml
+++ /dev/null
@@ -1,4 +0,0 @@
-open Raw
-
-module A = AbsImplicitt
-module R = RawSyntax
diff --git a/lib/Parse/dune b/lib/Parse/dune
deleted file mode 100644
index 746b65d..0000000
--- a/lib/Parse/dune
+++ /dev/null
@@ -1,12 +0,0 @@
-(library
- (name Parse)
- (libraries Raw)
- (flags (:standard -w -27 -w -39 -w -33)))
-
-(rule
-  (deps "implicitt.cf")
-  (targets AbsImplicitt.ml BNFC_Util.ml LexImplicitt.mll ParImplicitt.mly PrintImplicitt.ml ShowImplicitt.ml SkelImplicitt.ml TestImplicitt.ml)
-  (action (run bnfc --ocaml %{deps})))
-
-(ocamllex LexImplicitt)
-(ocamlyacc ParImplicitt)
diff --git a/lib/Parse/implicitt.cf b/lib/Parse/implicitt.cf
deleted file mode 100644
index 063bb30..0000000
--- a/lib/Parse/implicitt.cf
+++ /dev/null
@@ -1,62 +0,0 @@
-entrypoints [Def], Term;
-
-token Id ((letter|digit|["[]_"])+) ;
-
-comment "--" ;
-comment "{-" "-}" ;
-
-Defn. Def ::= "def" Id ":" Term ":=" Term;
-separator nonempty Def "" ;
-
--- names bound by lambdas
-NImp.   Name ::= "{" Id "}";
-NExp.   Name ::= Id;
-separator nonempty Name "" ;
-
--- Term 3
-TType.  Term3 ::= "Type";
-
-TT0.    Term3 ::= "𝟘";
-TInd0.  Term3 ::= "𝟘-elim";
-
-TT1.    Term3 ::= "𝟙";
-TT1tr.  Term3 ::= "★";
-
-TBool.  Term3 ::= "𝟚";
-TTrue.  Term3 ::= "true";
-TFalse. Term3 ::= "false";
-TIndB.  Term3 ::= "𝟚-elim";
-
-TNat.   Term3 ::= "ℕ";
-TZero.  Term3 ::= "0";
-TSuc.   Term3 ::= "suc";
-TIndN.  Term3 ::= "ℕ-elim";
-
-TFst.   Term3 ::= "pr₁";
-TSnd.   Term3 ::= "pr₂";
-
-TLam.   Term3 ::= "λ" [Name] "." Term;
-
-TVar.   Term3 ::= Id;
-
--- Term2
-
-TAppEx. Term2 ::= Term2 Term3;
-TAppIm. Term2 ::= Term2 "{" Term "}";
-
--- Term1
-TPiAr.  Term1 ::= Term2 "→" Term1;
-TSgCr.  Term1 ::= Term2 "×" Term1;
-
--- Term0
-TLet.   Term ::= "let" Id ":" Term ":=" Term "in" Term ;
-
-TPiEx.  Term ::= "(" Id ":" Term ")" "→" Term;
-TPiIm.  Term ::= "{" Id ":" Term "}" "→" Term;
-
-TSg.    Term ::= "(" Id ":" Term ")" "×" Term;
-TPair.  Term ::= "⟨" Term "," Term "⟩";
-
-THole.  Term ::= "?";
-
-coercions Term 3;