>Number:         20669
>Category:       pkg
>Synopsis:       New package lang/coq: Theorem prover which extracts programs from proofs
>Confidential:   no
>Severity:       serious
>Priority:       medium
>Responsible:    pkg-manager
>State:          open
>Class:          change-request
>Submitter-Id:   net
>Arrival-Date:   Wed Mar 12 01:14:01 PST 2003
>Closed-Date:
>Last-Modified:
>Originator:     Christopher Richards
>Release:        NetBSD 1.6.1_RC2
>Organization:
 
>Environment:
	
	
System: NetBSD zembla.Princeton.EDU 1.6.1_RC2 NetBSD 1.6.1_RC2 (ZEMBLA) #0: Thu Mar 6 05:20:48 EST 2003 richards@zembla.Princeton.EDU:/usr/src/sys/arch/i386/compile/ZEMBLA i386
Architecture: i386
Machine: i386
>Description:
	From http://coq.inria.fr/doc/tutorial.html:

	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.

>How-To-Repeat:
	
>Fix:
	Unpack <http://www.cs.princeton.edu/~richards/dist/coq-pkgsrc.tgz>
	in /usr/pkgsrc.
>Release-Note:
>Audit-Trail:
>Unformatted: