diff --git a/Make b/_CoqProject
similarity index 100%
rename from Make
rename to _CoqProject
diff --git a/configure.sh b/configure.sh
index bf5c524..9d71478 100755
--- a/configure.sh
+++ b/configure.sh
@@ -1,3 +1,3 @@
 #!/bin/sh
 
-coq_makefile -f Make -o Makefile
\ No newline at end of file
+coq_makefile -f _CoqProject -o Makefile
diff --git a/theories/Mtactics.v b/theories/Mtactics.v
index 8242a73..0e4694d 100644
--- a/theories/Mtactics.v
+++ b/theories/Mtactics.v
@@ -389,7 +389,8 @@ There is an issue with the
 *)
 Example test (x : nat) (y : nat) (H : x > y) : x > y.
 rrun (p <- match_goal ([? a] a => @assumption a)%mtac_patt; ret (snd p)).
-
+Qed.
+(*
 match goal with
 | [u:nat, v:nat, H : ?v > ?u |- _] => idtac v; apply I 
 end.