diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..9822e3e
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+*.lpo
diff --git a/Main.lp b/Main.lp
index 1963bec..ca4bd30 100644
--- a/Main.lp
+++ b/Main.lp
@@ -25,13 +25,3 @@ symbol Rnotall a p : (Π t : τ a, π (¬ (p t)) → π ⊥) → π (¬ (∀ p))
 symbol Rsubst a p (t1 t2 : τ a) : (π (¬ (t1 = t2)) → π ⊥) → (π (p t2) → π ⊥) → π (p t1) → π ⊥;
 symbol Rconglr a p (t1 t2 : τ a) : (π (p t2) → π ⊥) → π (p t1) → π (t1 = t2) → π ⊥;
 symbol Rcongrl a p (t1 t2 : τ a) : (π (p t2) → π ⊥) → π (p t1) → π (t2 = t1) → π ⊥;
-
-// temporary renamings to be removed ultimately
-symbol Type ≔ Set;
-symbol ι : Set;
-symbol τ ≔ τ;
-symbol κ ≔ τ ι;
-symbol ∀α [a] ≔ ∀ [a];
-symbol ∃α [a] ≔ ∃ [a];
-symbol =α [a] ≔ (=) [a];
-symbol ϵ ≔ π;
diff --git a/lambdapi-zenon.opam b/lambdapi-zenon.opam
index fdbd902..78dedf6 100644
--- a/lambdapi-zenon.opam
+++ b/lambdapi-zenon.opam
@@ -9,6 +9,7 @@ license: "CECILL-2.1"
 homepage: "https://github.com/Deducteam/lambdapi-zenon"
 bug-reports: "https://github.com/Deducteam/lambdapi-zenon/issues"
 dev-repo: "git+https://github.com/Deducteam/lambdapi-zenon.git"
+build: [ make ]
 install: [ make "install" ]
 depends: [
   "lambdapi" {>= "2.3.0"}