The Coq mailing list

[枫盛 <fsheng1990 AT 163.com>]

Hello everyone!

I use coq + emacs + proof-general to write coq file, but when I try to compile the file, it doesn’t work. The error is as following :

make test.vo

make: *** No rule to make target `test.vo'.  Stop.

Compilation exited abnormally with code 2 at Thu May 14 21:09:43

This is my file :

Definition pierce := forall (p q : Prop), ((p -> q) -> p) -> p.

Definition lem := forall (p : Prop), p \/ ~ p.

Theorem pierce_equiv_lem : pierce <-> lem.

Proof.

  unfold pierce, lem.

  firstorder.

  apply H with (q := ~(p \/ ~p)).

  tauto.

  destruct (H p).

  assumption.

  tauto.

Qed.