head	1.2;
access;
symbols
	pkgsrc-2013Q2:1.2.0.54
	pkgsrc-2013Q2-base:1.2
	pkgsrc-2012Q4:1.2.0.52
	pkgsrc-2012Q4-base:1.2
	pkgsrc-2011Q4:1.2.0.50
	pkgsrc-2011Q4-base:1.2
	pkgsrc-2011Q2:1.2.0.48
	pkgsrc-2011Q2-base:1.2
	pkgsrc-2009Q4:1.2.0.46
	pkgsrc-2009Q4-base:1.2
	pkgsrc-2008Q4:1.2.0.44
	pkgsrc-2008Q4-base:1.2
	pkgsrc-2008Q3:1.2.0.42
	pkgsrc-2008Q3-base:1.2
	cube-native-xorg:1.2.0.40
	cube-native-xorg-base:1.2
	pkgsrc-2008Q2:1.2.0.38
	pkgsrc-2008Q2-base:1.2
	pkgsrc-2008Q1:1.2.0.36
	pkgsrc-2008Q1-base:1.2
	pkgsrc-2007Q4:1.2.0.34
	pkgsrc-2007Q4-base:1.2
	pkgsrc-2007Q3:1.2.0.32
	pkgsrc-2007Q3-base:1.2
	pkgsrc-2007Q2:1.2.0.30
	pkgsrc-2007Q2-base:1.2
	pkgsrc-2007Q1:1.2.0.28
	pkgsrc-2007Q1-base:1.2
	pkgsrc-2006Q4:1.2.0.26
	pkgsrc-2006Q4-base:1.2
	pkgsrc-2006Q3:1.2.0.24
	pkgsrc-2006Q3-base:1.2
	pkgsrc-2006Q2:1.2.0.22
	pkgsrc-2006Q2-base:1.2
	pkgsrc-2006Q1:1.2.0.20
	pkgsrc-2006Q1-base:1.2
	pkgsrc-2005Q4:1.2.0.18
	pkgsrc-2005Q4-base:1.2
	pkgsrc-2005Q3:1.2.0.16
	pkgsrc-2005Q3-base:1.2
	pkgsrc-2005Q2:1.2.0.14
	pkgsrc-2005Q2-base:1.2
	pkgsrc-2005Q1:1.2.0.12
	pkgsrc-2005Q1-base:1.2
	pkgsrc-2004Q4:1.2.0.10
	pkgsrc-2004Q4-base:1.2
	pkgsrc-2004Q3:1.2.0.8
	pkgsrc-2004Q3-base:1.2
	pkgsrc-2004Q2:1.2.0.6
	pkgsrc-2004Q2-base:1.2
	pkgsrc-2004Q1:1.2.0.4
	pkgsrc-2004Q1-base:1.2
	pkgsrc-2003Q4:1.2.0.2
	pkgsrc-2003Q4-base:1.2
	pkgsrc-base:1.1.1.1
	TNF:1.1.1;
locks; strict;
comment	@# @;


1.2
date	2003.03.22.20.16.06;	author kristerw;	state dead;
branches;
next	1.1;

1.1
date	2003.03.22.18.20.54;	author kristerw;	state Exp;
branches
	1.1.1.1;
next	;

1.1.1.1
date	2003.03.22.18.20.54;	author kristerw;	state Exp;
branches;
next	;


desc
@@


1.2
log
@By popular demand, move coq from math to lang in order to be consistent
with prior art (e.g. lang/twelf).
@
text
@# $NetBSD: Makefile,v 1.1 2003/03/22 18:20:54 kristerw Exp $
#

DISTNAME=	coq-7.4
CATEGORIES=	math lang
MASTER_SITES=	ftp://ftp.inria.fr/INRIA/coq/V7.4/

MAINTAINER=	richards+netbsd@@CS.Princeton.EDU
HOMEPAGE=	http://coq.inria.fr/
COMMENT=	Theorem prover which extracts programs from proofs

USE_GMAKE=	YES
USE_BUILDLINK2=	YES
HAS_CONFIGURE=	YES
CONFIGURE_ARGS+=	-prefix ${PREFIX}
CONFIGURE_ARGS+=	-emacslib ${PREFIX}/share/emacs/site-lisp
CONFIGURE_ARGS+=	-reals all
ALL_TARGET=	world

.include "../../mk/bsd.prefs.mk"

.if (${MACHINE_ARCH} == "i386")
PLIST_SRC=	${PKGDIR}/PLIST.opt ${PKGDIR}/PLIST
.endif

.include "../../lang/ocaml/buildlink2.mk"
.include "../../mk/bsd.pkg.mk"
@


1.1
log
@Initial revision
@
text
@d1 1
a1 1
# $NetBSD$
@


1.1.1.1
log
@Import coq 7.4. From Christopher Richards in PR 20669.

    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.
@
text
@@