diff --git a/Makefile b/Makefile
index f3609c292..ee9fde1a1 100644
--- a/Makefile
+++ b/Makefile
@@ -22,6 +22,7 @@ clean: Makefile.coq Makefile.coqplugin Makefile.coqchecker
 	$(MAKE) -f Makefile.coq clean
 	$(MAKE) -f Makefile.coqplugin clean
 	$(MAKE) -f Makefile.coqchecker clean
+	rm -rf theories/Extraction.glob theories/Extraction.vo theories/TypingPlugin.glob theories/TypingPlugin.vo
 	git checkout html/coqdoc.css
 
 mrproper: clean
diff --git a/theories/Ast.v b/theories/Ast.v
index b7a0b4341..c847de0ee 100644
--- a/theories/Ast.v
+++ b/theories/Ast.v
@@ -271,7 +271,7 @@ Inductive global_reference :=
 
 (** *** The TemplateMonad type *)
 
-Inductive TemplateMonad : Type -> Prop :=
+Inductive TemplateMonad : Type -> Type :=
 (* Monadic operations *)
 | tmReturn : forall {A:Type}, A -> TemplateMonad A
 | tmBind : forall {A B : Type}, TemplateMonad A -> (A -> TemplateMonad B)