fixing build issue.

beta-ziliani · Oct 6, 2015 · e82e7ee · e82e7ee
1 parent 39a3a25
commit e82e7ee
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 2 deletions.
diff --git a/Make → _CoqProject b/Make → _CoqProject
diff --git a/configure.sh b/configure.sh
@@ -1,3 +1,3 @@
 #!/bin/sh
 
-coq_makefile -f Make -o Makefile
+coq_makefile -f _CoqProject -o Makefile
diff --git 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.