pkgsrc

kpriv/pkgsrc

Fork 0

Commit graph

Author	SHA1	Message	Date
jtb	b683565843	Build with native code compilers on systems where they're available, which now includes powerpc and sparc. Bump PKGREVISION.	2003-06-23 20:36:13 +00:00
kristerw	358f2678e5	By popular demand, move coq-7.4 from math to lang in order to be consistent with prior art (e.g. lang/twelf). Coq is a Proof Assistant for a Logical Framework known as the Calculus of Inductive Constructions. It allows the interactive construction of formal proofs, and also the manipulation of functional programs consistently with their specifications.	2003-03-22 20:21:16 +00:00

Author

SHA1

Message

Date

jtb

b683565843

Build with native code compilers on systems where they're available,

which now includes powerpc and sparc.
Bump PKGREVISION.

2003-06-23 20:36:13 +00:00

kristerw

358f2678e5

By popular demand, move coq-7.4 from math to lang in order to be consistent

with prior art (e.g. lang/twelf).

    Coq is a Proof Assistant for a Logical Framework known as the
    Calculus of Inductive Constructions. It allows the interactive
    construction of formal proofs, and also the manipulation of
    functional programs consistently with their specifications.

2003-03-22 20:21:16 +00:00

2 commits