Merge pull request #30 from Template-Coq/templatemonad-prop

Move TemplateMonad from Prop to Type
gmalecha · May 2, 2018 · a81bd81 · a81bd81
2 parents 2d02d18 + 04ad1e0
commit a81bd81
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git 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
@@ -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)