Skip to content

Instantly share code, notes, and snippets.

@clairvy

clairvy/Makefile

Created August 8, 2010 22:15
Show Gist options
  • Save clairvy/514622 to your computer and use it in GitHub Desktop.
Save clairvy/514622 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Makefile
default: check
check : a.v
coqc a.v
a.v : Theorems.v
( cat Theorems.v ; echo ; echo 'Definition check_Modus_ponens: forall (P Q: Prop), (P -> Q) -> P -> Q := Modus_ponens.' ) > a.v
clean:
$(RM) $(RMF) a.v a.glob a.vo
Raw
Theorems.v
Fact Modus_ponens:forall(P Q:Prop),(P->Q)->P->Q.
auto.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment