Revert "Add some templates (#91)"

This reverts commit 0cf0b62.

theories/Core/Completeness.v

@@ -4,7 +4,7 @@ Import Domain_Notations.
 
 Theorem completeness : forall {Γ M M' A},
   {{ Γ ⊢ M ≈ M' : A }} ->
-  exists W, nbe Γ M A W /\ nbe Γ M' A W.
+  exists m, nbe Γ M A m /\ nbe Γ M' A m.
 Proof with mautosolve.
   intros * [env_relΓ]%completeness_fundamental_exp_eq.
   destruct_conjs.

theories/Core/Semantic/NbE.v

@@ -1,6 +1,5 @@
 From Mcltt Require Import Base LibTactics.
 From Mcltt.Core Require Import Evaluation Readback.
-From Mcltt.Core Require Export Domain.
 Import Domain_Notations.
 
 Generalizable All Variables.
@@ -61,14 +60,3 @@ Proof.
   functional_read_rewrite_clear;
   reflexivity.
 Qed.
-
-#[export]
-Hint Resolve functional_nbe : mcltt.
-
-Ltac functional_nbe_rewrite_clear1 :=
-  let tactic_error o1 o2 := fail 3 "functional_nbe equality between" o1 "and" o2 "cannot be solved by mauto" in
-  match goal with
-  | H1 : nbe ?G ?M ?A ?W, H2 : nbe ?G ?M ?A ?W' |- _ =>
-      clean replace W' with W by first [solve [mauto] | tactic_error W' W]; clear H2
-  end.
-Ltac functional_nbe_rewrite_clear := repeat functional_nbe_rewrite_clear1.

theories/Core/Syntactic/Syntax.v

@@ -99,15 +99,6 @@ with ne_to_exp (M : ne) : exp :=
 Coercion nf_to_exp : nf >-> exp.
 Coercion ne_to_exp : ne >-> exp.
 
-Fact nf_eq_dec : forall (M M' : nf),
-    ({M = M'} + {M <> M'})%type
-with ne_eq_dec : forall (M M' : ne),
-    ({M = M'} + {M <> M'})%type.
-Proof.
-  all: intros; decide equality;
-    apply PeanoNat.Nat.eq_dec.
-Defined.
-
 #[global] Declare Custom Entry exp.
 #[global] Declare Custom Entry nf.
 

theories/_CoqProject

@@ -37,7 +37,6 @@
 ./Core/Syntactic/System.v
 ./Core/Syntactic/System/Definitions.v
 ./Core/Syntactic/System/Lemmas.v
-./Core/Soundness.v
 ./Core/Soundness/LogicalRelation.v
 ./Core/Soundness/Weakening.v
 ./Core/Soundness/Weakening/Definition.v
@@ -46,7 +45,6 @@
 ./Frontend/Parser.v
 ./Frontend/ParserExtraction.v
 ./Extraction/Evaluation.v
-./Extraction/NbE.v
 ./Extraction/Readback.v
-./Extraction/TypeCheck.v
+./Extraction/NbE.v
 ./LibTactics.v