diff --git a/template-coq/Makefile b/template-coq/Makefile
index 9aa736658..ddde08bbb 100644
--- a/template-coq/Makefile
+++ b/template-coq/Makefile
@@ -1,4 +1,4 @@
-all: coq plugin
+all: coq # plugin
 
 coq: Makefile.coq
 	$(MAKE) -f Makefile.coq
diff --git a/template-coq/test-plugin/test.v b/template-coq/test-plugin/test.v
deleted file mode 100644
index bd2287f22..000000000
--- a/template-coq/test-plugin/test.v
+++ /dev/null
@@ -1 +0,0 @@
-Declare ML Module "meta_coq_plugin_template".
\ No newline at end of file
diff --git a/template-coq/theories/All.v b/template-coq/theories/All.v
index c1f8243cb..39588f3f3 100644
--- a/template-coq/theories/All.v
+++ b/template-coq/theories/All.v
@@ -8,7 +8,7 @@ From MetaCoq.Template Require Export
      uGraph        (* The graph of universes *)
      TemplateMonad (* The TemplateMonad *)
      AstUtils      (* Utilities on the AST *)
-     Loader        (* Declaration of the Template Coq plugin *)
+     (* Loader        (* Declaration of the Template Coq plugin *) *)
      Induction     (* Induction *)
      LiftSubst     (* Lifting and substitution for terms *)
      UnivSubst     (* Substitution of universe instances *)
diff --git a/template-coq/theories/Extraction.v b/template-coq/theories/Extraction.v
deleted file mode 100644
index 2876efd10..000000000
--- a/template-coq/theories/Extraction.v
+++ /dev/null
@@ -1,32 +0,0 @@
-(** Extraction setup for template-coq.
-
-    Any extracted code planning to link with the plugin's OCaml reifier
-    should use these same directives for consistency.
-*)
-
-(* From MetaCoq.Template Require All. *)
-Require Import MetaCoq.Template.utils.
-Require Import FSets.
-Require Import ExtrOcamlBasic.
-Require Import ExtrOcamlString ExtrOcamlZInt.
-
-(* Ignore [Decimal.int] before the extraction issue is solved:
-   https://github.com/coq/coq/issues/7017. *)
-Extract Inductive Decimal.int => unit [ "(fun _ -> ())" "(fun _ -> ())" ] "(fun _ _ _ -> assert false)".
-
-Extract Constant utils.ascii_compare =>
- "fun x y -> match Char.compare x y with 0 -> Eq | x when x < 0 -> Lt | _ -> Gt".
-
-Extraction Blacklist config uGraph Universes Ast String List Nat Int
-           UnivSubst Typing Checker Retyping OrderedType Logic Common.
-Set Warnings "-extraction-opaque-accessed".
-
-Require Export MetaCoq.Template.Ast.
-
-Cd "gen-src".
-
-Require Import MetaCoq.Template.TemplateMonad.Extractable.
-
-Recursive Extraction Library Extractable.
-
-Cd "..".
\ No newline at end of file
diff --git a/template-coq/theories/Loader.v b/template-coq/theories/Loader.v
deleted file mode 100644
index a1ecc8ac9..000000000
--- a/template-coq/theories/Loader.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Template.TemplateMonad.Core.
-Require Template.TemplateMonad.Extractable.
-
-Declare ML Module "template_coq".
\ No newline at end of file
diff --git a/template-coq/theories/Validity.v b/template-coq/theories/Validity.v
deleted file mode 100644
index 11b839da4..000000000
--- a/template-coq/theories/Validity.v
+++ /dev/null
@@ -1,62 +0,0 @@
-From Coq Require Import Bool String List Program BinPos Compare_dec Omega.
-From MetaCoq.Template Require Import config utils Ast AstUtils Induction LiftSubst Typing WeakSubst.
-
-Arguments All_local_env typing%type_scope {H} Σ Γ.
-
-Definition on_local_decl P Σ d :=
-  match d.(decl_body) with
-  | None => {s : universe & { Γ' & isType Σ Γ' d.(decl_type)
-  | Some body => Σ ;;; Γ |- body : d.(decl_type)
-  end.
-
-
-Lemma All_local_env_lookup `{checker_flags} P Q Σ Γ n (isdecl : n < #|Γ|) :
-  All_local_env P Σ Γ -> on_decl_typing P (safe_nth Γ (exist _ n isdecl))
-Proof.
-  induction 1. constructor.
-  intros. inv X0; auto. econstructor; auto.
-  split; eauto.
-
-Lemma type_local_env_isdecl `{checker_flags} Σ n Γ :
-  forall isdecl : n < #|Γ|, wf_local Σ Γ ->
-  { Γ' : _ & { Γ'' : _ &
-                    { _ : type_local_decl Σ Γ'' (safe_nth Γ (exist _ n isdecl)) &
-                    Γ = (Γ' ++ Γ'')%list /\ #|Γ'| = S n } } }.
-Proof. Admitted.
-
-Definition isSort T :=
-  match T with
-  | tSort _ => true
-  | _ => false
-  end.
-
-Theorem validity `{checker_flags} : env_prop (fun Σ Γ t T => ((isSort T = true) + isType Σ Γ T)%type).
-Proof.
-  apply typing_ind_env; intros.
-
-  - pose proof wfΓ as H0.
-    apply (type_local_env_isdecl _ _ _ isdecl) in H0 as [Γ' [Γ'' [H0 [-> <-]]]].
-    destruct safe_nth. simpl in *.
-    red in H0. simpl in H0. destruct decl_body.
-    Lemma All_local_env_decl
-
-    admit.
-    destruct H0. right; exists x.
-    now refine (weakening _ _ _ _ _ _ _ t).
-
-  - left; reflexivity.
-  - right; now exists s.
-  - left; reflexivity.
-  - right. econstructor. constructor; eauto.
-    destruct X2.
-    destruct H2 as [s Hs]. constructor. auto. 
-    eexists. eauto.
-    (* Aha: need alpha-conv on local assumptions... *)
-    admit.
-
-  - admit.
-  - admit.
-  - (* Easy now *)
-Admitted.
-
-Eval compute in validity.