Import of coq 7.0.
Submitted by Yozo Toda <yozo@imit.chiba-u.ac.jp>. The Coq Proof Assistant is designed to write formal specifications, programs and to verify that programs are correct with respect to their specification.
This commit is contained in:
naddy
parent
97a674092c
commit
3367255cb4
51
math/coq/Makefile
Normal file
51
math/coq/Makefile
Normal file
@ -0,0 +1,51 @@
|
||||
# $OpenBSD: Makefile,v 1.1.1.1 2001/09/22 14:24:31 naddy Exp $
|
||||
|
||||
COMMENT= "proof assistant based on a typed lambda calculus"
|
||||
|
||||
DISTNAME= coq-7.0
|
||||
CATEGORIES= math
|
||||
NEED_VERSION= 1.457
|
||||
HOMEPAGE= http://coq.inria.fr/
|
||||
|
||||
MAINTAINER= Yozo Toda <yozo@imit.chiba-u.ac.jp>
|
||||
|
||||
PERMIT_PACKAGE_CDROM= Yes
|
||||
PERMIT_PACKAGE_FTP= Yes
|
||||
PERMIT_DISTFILES_CDROM= Yes
|
||||
PERMIT_DISTFILES_FTP= Yes
|
||||
|
||||
MASTER_SITES= ftp://ftp.inria.fr/INRIA/coq/V7.0/ \
|
||||
ftp://ftp.imit.chiba-u.ac.jp/pub/pub.yozo/tmp/ftp.inria.fr/INRIA/Projects/coq/coq/V7.0/
|
||||
MASTER_SITES0= ${MASTER_SITES:S@$@doc/@}
|
||||
DISTFILES= ${DISTNAME}.tar.gz \
|
||||
doc-html.tar.gz:0 \
|
||||
all-ps-docs.tar.gz:0
|
||||
DIST_SUBDIR= coq
|
||||
|
||||
BUILD_DEPENDS= ocamlc::lang/ocaml \
|
||||
camlp4::lang/camlp4
|
||||
|
||||
FAKE_FLAGS= COQINSTALLPREFIX=${WRKINST}
|
||||
|
||||
USE_GMAKE= Yes
|
||||
|
||||
CONFIGURE_STYLE= simple
|
||||
## add -opt option if there is ocamlc.opt.
|
||||
CONFIGURE_ARGS= -prefix ${PREFIX} \
|
||||
-emacslib ${PREFIX}/share/emacs/site-lisp ## -opt
|
||||
|
||||
ALL_TARGET= world
|
||||
|
||||
COQ_DOCPSFILES= Changes.ps Library.ps Tutorial.ps \
|
||||
Reference-Manual-addendum.ps Reference-Manual-base.ps
|
||||
|
||||
post-install:
|
||||
@${INSTALL_DATA_DIR} ${PREFIX}/share/doc/coq/html
|
||||
@${INSTALL_DATA} ${WRKDIR}/coq-docs-html/* ${PREFIX}/share/doc/coq/html
|
||||
@${INSTALL_DATA_DIR} ${PREFIX}/share/doc/coq/ps
|
||||
@for ff in ${COQ_DOCPSFILES} ; do \
|
||||
${INSTALL_DATA} ${WRKDIR}/$${ff} ${PREFIX}/share/doc/coq/ps ; \
|
||||
done
|
||||
@strip ${PREFIX}/bin/*
|
||||
|
||||
.include <bsd.port.mk>
|
||||
9
math/coq/files/md5
Normal file
9
math/coq/files/md5
Normal file
@ -0,0 +1,9 @@
|
||||
MD5 (coq/coq-7.0.tar.gz) = d0ac03af950acd27b3313043e5aa3587
|
||||
MD5 (coq/all-ps-docs.tar.gz) = 1bdcea2bf45707c8d542c5cdcd2dbbf6
|
||||
MD5 (coq/doc-html.tar.gz) = 802b110114e54068b502f37c8156cdf2
|
||||
RMD160 (coq/coq-7.0.tar.gz) = d3139881574f83935292e71014d1c54c260c1787
|
||||
RMD160 (coq/all-ps-docs.tar.gz) = c3aa484984949eaf0fd5aa5c1e7087aee6900dad
|
||||
RMD160 (coq/doc-html.tar.gz) = 75df7f07af08c97c0cb4286ccfb03d656e3d3c08
|
||||
SHA1 (coq/coq-7.0.tar.gz) = e550d2cc92df0813c2f16c151ab3eae6c2c6acb6
|
||||
SHA1 (coq/all-ps-docs.tar.gz) = 693187982509dec281d9d9cd028d78e812d30cf2
|
||||
SHA1 (coq/doc-html.tar.gz) = 3cfbcc6756cc9b30451cef07094a3c1f8a2cb7bf
|
||||
4
math/coq/pkg/DESCR
Normal file
4
math/coq/pkg/DESCR
Normal file
@ -0,0 +1,4 @@
|
||||
The Coq Proof Assistant is designed to write formal specifications, programs
|
||||
and to verify that programs are correct with respect to their specification.
|
||||
|
||||
WWW: ${HOMEPAGE}
|
||||
376
math/coq/pkg/PLIST
Normal file
376
math/coq/pkg/PLIST
Normal file
@ -0,0 +1,376 @@
|
||||
@comment $OpenBSD: PLIST,v 1.1.1.1 2001/09/22 14:24:31 naddy Exp $
|
||||
bin/coq-interface
|
||||
bin/coq-tex
|
||||
bin/coq_makefile
|
||||
bin/coqc
|
||||
bin/coqdep
|
||||
bin/coqmktop
|
||||
bin/coqtop
|
||||
bin/coqtop.byte
|
||||
bin/coqtop.opt
|
||||
bin/gallina
|
||||
bin/parser
|
||||
lib/coq/contrib/correctness/ArrayPermut.vo
|
||||
lib/coq/contrib/correctness/Arrays.vo
|
||||
lib/coq/contrib/correctness/Correctness.vo
|
||||
lib/coq/contrib/correctness/Exchange.vo
|
||||
lib/coq/contrib/correctness/ProgBool.vo
|
||||
lib/coq/contrib/correctness/ProgInt.vo
|
||||
lib/coq/contrib/correctness/ProgWf.vo
|
||||
lib/coq/contrib/correctness/Sorted.vo
|
||||
lib/coq/contrib/correctness/Tuples.vo
|
||||
lib/coq/contrib/extraction/Extraction.vo
|
||||
lib/coq/contrib/field/Field.vo
|
||||
lib/coq/contrib/field/Field_Compl.vo
|
||||
lib/coq/contrib/field/Field_Tactic.vo
|
||||
lib/coq/contrib/field/Field_Theory.vo
|
||||
lib/coq/contrib/fourier/Fourier.vo
|
||||
lib/coq/contrib/fourier/Fourier_util.vo
|
||||
lib/coq/contrib/interface/Centaur.vo
|
||||
lib/coq/contrib/interface/vernacrc
|
||||
lib/coq/contrib/omega/Omega.vo
|
||||
lib/coq/contrib/omega/OmegaSyntax.vo
|
||||
lib/coq/contrib/omega/Zcomplements.vo
|
||||
lib/coq/contrib/omega/Zlogarithm.vo
|
||||
lib/coq/contrib/omega/Zpower.vo
|
||||
lib/coq/contrib/ring/ArithRing.vo
|
||||
lib/coq/contrib/ring/Quote.vo
|
||||
lib/coq/contrib/ring/Ring.vo
|
||||
lib/coq/contrib/ring/Ring_abstract.vo
|
||||
lib/coq/contrib/ring/Ring_normalize.vo
|
||||
lib/coq/contrib/ring/Ring_theory.vo
|
||||
lib/coq/contrib/ring/ZArithRing.vo
|
||||
lib/coq/contrib/xml/Xml.vo
|
||||
lib/coq/states/barestate.coq
|
||||
lib/coq/states/initial.coq
|
||||
lib/coq/tactics/AutoRewrite.vo
|
||||
lib/coq/tactics/EAuto.vo
|
||||
lib/coq/tactics/EqDecide.vo
|
||||
lib/coq/tactics/Equality.vo
|
||||
lib/coq/tactics/Inv.vo
|
||||
lib/coq/tactics/Refine.vo
|
||||
lib/coq/tactics/Tauto.vo
|
||||
lib/coq/theories/Arith/Arith.vo
|
||||
lib/coq/theories/Arith/Between.vo
|
||||
lib/coq/theories/Arith/Compare.vo
|
||||
lib/coq/theories/Arith/Compare_dec.vo
|
||||
lib/coq/theories/Arith/Div2.vo
|
||||
lib/coq/theories/Arith/EqNat.vo
|
||||
lib/coq/theories/Arith/Euclid.vo
|
||||
lib/coq/theories/Arith/Even.vo
|
||||
lib/coq/theories/Arith/Gt.vo
|
||||
lib/coq/theories/Arith/Le.vo
|
||||
lib/coq/theories/Arith/Lt.vo
|
||||
lib/coq/theories/Arith/Min.vo
|
||||
lib/coq/theories/Arith/Minus.vo
|
||||
lib/coq/theories/Arith/Mult.vo
|
||||
lib/coq/theories/Arith/Peano_dec.vo
|
||||
lib/coq/theories/Arith/Plus.vo
|
||||
lib/coq/theories/Arith/Wf_nat.vo
|
||||
lib/coq/theories/Bool/Bool.vo
|
||||
lib/coq/theories/Bool/BoolEq.vo
|
||||
lib/coq/theories/Bool/DecBool.vo
|
||||
lib/coq/theories/Bool/IfProp.vo
|
||||
lib/coq/theories/Bool/Sumbool.vo
|
||||
lib/coq/theories/Bool/Zerob.vo
|
||||
lib/coq/theories/Init/Datatypes.vo
|
||||
lib/coq/theories/Init/DatatypesSyntax.vo
|
||||
lib/coq/theories/Init/Logic.vo
|
||||
lib/coq/theories/Init/LogicSyntax.vo
|
||||
lib/coq/theories/Init/Logic_Type.vo
|
||||
lib/coq/theories/Init/Logic_TypeSyntax.vo
|
||||
lib/coq/theories/Init/Peano.vo
|
||||
lib/coq/theories/Init/Prelude.vo
|
||||
lib/coq/theories/Init/Specif.vo
|
||||
lib/coq/theories/Init/SpecifSyntax.vo
|
||||
lib/coq/theories/Init/Wf.vo
|
||||
lib/coq/theories/IntMap/Adalloc.vo
|
||||
lib/coq/theories/IntMap/Addec.vo
|
||||
lib/coq/theories/IntMap/Addr.vo
|
||||
lib/coq/theories/IntMap/Adist.vo
|
||||
lib/coq/theories/IntMap/Allmaps.vo
|
||||
lib/coq/theories/IntMap/Fset.vo
|
||||
lib/coq/theories/IntMap/Lsort.vo
|
||||
lib/coq/theories/IntMap/Map.vo
|
||||
lib/coq/theories/IntMap/Mapaxioms.vo
|
||||
lib/coq/theories/IntMap/Mapc.vo
|
||||
lib/coq/theories/IntMap/Mapcanon.vo
|
||||
lib/coq/theories/IntMap/Mapcard.vo
|
||||
lib/coq/theories/IntMap/Mapfold.vo
|
||||
lib/coq/theories/IntMap/Mapiter.vo
|
||||
lib/coq/theories/IntMap/Maplists.vo
|
||||
lib/coq/theories/IntMap/Mapsubset.vo
|
||||
lib/coq/theories/Lists/List.vo
|
||||
lib/coq/theories/Lists/ListSet.vo
|
||||
lib/coq/theories/Lists/PolyList.vo
|
||||
lib/coq/theories/Lists/PolyListSyntax.vo
|
||||
lib/coq/theories/Lists/Streams.vo
|
||||
lib/coq/theories/Lists/TheoryList.vo
|
||||
lib/coq/theories/Logic/Classical.vo
|
||||
lib/coq/theories/Logic/Classical_Pred_Set.vo
|
||||
lib/coq/theories/Logic/Classical_Pred_Type.vo
|
||||
lib/coq/theories/Logic/Classical_Prop.vo
|
||||
lib/coq/theories/Logic/Classical_Type.vo
|
||||
lib/coq/theories/Logic/Decidable.vo
|
||||
lib/coq/theories/Logic/Eqdep.vo
|
||||
lib/coq/theories/Logic/Eqdep_dec.vo
|
||||
lib/coq/theories/Logic/JMeq.vo
|
||||
lib/coq/theories/Reals/DiscrR.vo
|
||||
lib/coq/theories/Reals/R_Ifp.vo
|
||||
lib/coq/theories/Reals/Raxioms.vo
|
||||
lib/coq/theories/Reals/Rbase.vo
|
||||
lib/coq/theories/Reals/Rbasic_fun.vo
|
||||
lib/coq/theories/Reals/Rdefinitions.vo
|
||||
lib/coq/theories/Reals/Rderiv.vo
|
||||
lib/coq/theories/Reals/Reals.vo
|
||||
lib/coq/theories/Reals/Rfunctions.vo
|
||||
lib/coq/theories/Reals/Rlimit.vo
|
||||
lib/coq/theories/Reals/Rseries.vo
|
||||
lib/coq/theories/Reals/Rsyntax.vo
|
||||
lib/coq/theories/Reals/Rtrigo_fun.vo
|
||||
lib/coq/theories/Reals/SplitAbsolu.vo
|
||||
lib/coq/theories/Reals/SplitRmult.vo
|
||||
lib/coq/theories/Reals/TypeSyntax.vo
|
||||
lib/coq/theories/Relations/Newman.vo
|
||||
lib/coq/theories/Relations/Operators_Properties.vo
|
||||
lib/coq/theories/Relations/Relation_Definitions.vo
|
||||
lib/coq/theories/Relations/Relation_Operators.vo
|
||||
lib/coq/theories/Relations/Relations.vo
|
||||
lib/coq/theories/Relations/Rstar.vo
|
||||
lib/coq/theories/Sets/Classical_sets.vo
|
||||
lib/coq/theories/Sets/Constructive_sets.vo
|
||||
lib/coq/theories/Sets/Cpo.vo
|
||||
lib/coq/theories/Sets/Ensembles.vo
|
||||
lib/coq/theories/Sets/Finite_sets.vo
|
||||
lib/coq/theories/Sets/Finite_sets_facts.vo
|
||||
lib/coq/theories/Sets/Image.vo
|
||||
lib/coq/theories/Sets/Infinite_sets.vo
|
||||
lib/coq/theories/Sets/Integers.vo
|
||||
lib/coq/theories/Sets/Multiset.vo
|
||||
lib/coq/theories/Sets/Partial_Order.vo
|
||||
lib/coq/theories/Sets/Permut.vo
|
||||
lib/coq/theories/Sets/Powerset.vo
|
||||
lib/coq/theories/Sets/Powerset_Classical_facts.vo
|
||||
lib/coq/theories/Sets/Powerset_facts.vo
|
||||
lib/coq/theories/Sets/Relations_1.vo
|
||||
lib/coq/theories/Sets/Relations_1_facts.vo
|
||||
lib/coq/theories/Sets/Relations_2.vo
|
||||
lib/coq/theories/Sets/Relations_2_facts.vo
|
||||
lib/coq/theories/Sets/Relations_3.vo
|
||||
lib/coq/theories/Sets/Relations_3_facts.vo
|
||||
lib/coq/theories/Sets/Uniset.vo
|
||||
lib/coq/theories/Wellfounded/Disjoint_Union.vo
|
||||
lib/coq/theories/Wellfounded/Inclusion.vo
|
||||
lib/coq/theories/Wellfounded/Inverse_Image.vo
|
||||
lib/coq/theories/Wellfounded/Lexicographic_Exponentiation.vo
|
||||
lib/coq/theories/Wellfounded/Lexicographic_Product.vo
|
||||
lib/coq/theories/Wellfounded/Transitive_Closure.vo
|
||||
lib/coq/theories/Wellfounded/Union.vo
|
||||
lib/coq/theories/Wellfounded/Well_Ordering.vo
|
||||
lib/coq/theories/Wellfounded/Wellfounded.vo
|
||||
lib/coq/theories/ZArith/Wf_Z.vo
|
||||
lib/coq/theories/ZArith/ZArith.vo
|
||||
lib/coq/theories/ZArith/ZArith_dec.vo
|
||||
lib/coq/theories/ZArith/Zmisc.vo
|
||||
lib/coq/theories/ZArith/Zsyntax.vo
|
||||
lib/coq/theories/ZArith/auxiliary.vo
|
||||
lib/coq/theories/ZArith/fast_integer.vo
|
||||
lib/coq/theories/ZArith/zarith_aux.vo
|
||||
man/man1/coq-interface.1
|
||||
man/man1/coq-tex.1
|
||||
man/man1/coq_makefile.1
|
||||
man/man1/coqc.1
|
||||
man/man1/coqdep.1
|
||||
man/man1/coqmktop.1
|
||||
man/man1/coqtop.1
|
||||
man/man1/coqtop.byte.1
|
||||
man/man1/coqtop.opt.1
|
||||
man/man1/gallina.1
|
||||
man/man1/parser.1
|
||||
share/doc/coq/html/Library.html
|
||||
share/doc/coq/html/changes.html
|
||||
share/doc/coq/html/cover.html
|
||||
share/doc/coq/html/main-0.html
|
||||
share/doc/coq/html/main.html
|
||||
share/doc/coq/html/next.gif
|
||||
share/doc/coq/html/node.0.0.0.html
|
||||
share/doc/coq/html/node.0.0.1.html
|
||||
share/doc/coq/html/node.0.0.2.html
|
||||
share/doc/coq/html/node.0.0.html
|
||||
share/doc/coq/html/node.0.1.0.html
|
||||
share/doc/coq/html/node.0.1.1.html
|
||||
share/doc/coq/html/node.0.1.2.html
|
||||
share/doc/coq/html/node.0.1.3.html
|
||||
share/doc/coq/html/node.0.1.4.html
|
||||
share/doc/coq/html/node.0.1.5.html
|
||||
share/doc/coq/html/node.0.1.6.html
|
||||
share/doc/coq/html/node.0.1.html
|
||||
share/doc/coq/html/node.0.2.0.html
|
||||
share/doc/coq/html/node.0.2.1.html
|
||||
share/doc/coq/html/node.0.2.2.html
|
||||
share/doc/coq/html/node.0.2.html
|
||||
share/doc/coq/html/node.0.3.0.html
|
||||
share/doc/coq/html/node.0.3.1.html
|
||||
share/doc/coq/html/node.0.3.2.html
|
||||
share/doc/coq/html/node.0.3.3.html
|
||||
share/doc/coq/html/node.0.3.4.html
|
||||
share/doc/coq/html/node.0.3.5.html
|
||||
share/doc/coq/html/node.0.3.html
|
||||
share/doc/coq/html/node.0.html
|
||||
share/doc/coq/html/node.1.0.0.html
|
||||
share/doc/coq/html/node.1.0.1.html
|
||||
share/doc/coq/html/node.1.0.2.html
|
||||
share/doc/coq/html/node.1.0.3.html
|
||||
share/doc/coq/html/node.1.0.4.html
|
||||
share/doc/coq/html/node.1.0.5.html
|
||||
share/doc/coq/html/node.1.0.6.html
|
||||
share/doc/coq/html/node.1.0.7.html
|
||||
share/doc/coq/html/node.1.0.html
|
||||
share/doc/coq/html/node.1.1.0.html
|
||||
share/doc/coq/html/node.1.1.1.html
|
||||
share/doc/coq/html/node.1.1.2.html
|
||||
share/doc/coq/html/node.1.1.html
|
||||
share/doc/coq/html/node.1.2.0.html
|
||||
share/doc/coq/html/node.1.2.1.html
|
||||
share/doc/coq/html/node.1.2.10.html
|
||||
share/doc/coq/html/node.1.2.11.html
|
||||
share/doc/coq/html/node.1.2.12.html
|
||||
share/doc/coq/html/node.1.2.13.html
|
||||
share/doc/coq/html/node.1.2.14.html
|
||||
share/doc/coq/html/node.1.2.2.html
|
||||
share/doc/coq/html/node.1.2.3.html
|
||||
share/doc/coq/html/node.1.2.4.html
|
||||
share/doc/coq/html/node.1.2.5.html
|
||||
share/doc/coq/html/node.1.2.6.html
|
||||
share/doc/coq/html/node.1.2.7.html
|
||||
share/doc/coq/html/node.1.2.8.html
|
||||
share/doc/coq/html/node.1.2.9.html
|
||||
share/doc/coq/html/node.1.2.html
|
||||
share/doc/coq/html/node.1.3.0.html
|
||||
share/doc/coq/html/node.1.3.1.html
|
||||
share/doc/coq/html/node.1.3.2.html
|
||||
share/doc/coq/html/node.1.3.3.html
|
||||
share/doc/coq/html/node.1.3.4.html
|
||||
share/doc/coq/html/node.1.3.5.html
|
||||
share/doc/coq/html/node.1.3.html
|
||||
share/doc/coq/html/node.1.html
|
||||
share/doc/coq/html/node.2.0.0.html
|
||||
share/doc/coq/html/node.2.0.1.html
|
||||
share/doc/coq/html/node.2.0.2.html
|
||||
share/doc/coq/html/node.2.0.html
|
||||
share/doc/coq/html/node.2.1.0.html
|
||||
share/doc/coq/html/node.2.1.1.html
|
||||
share/doc/coq/html/node.2.1.2.html
|
||||
share/doc/coq/html/node.2.1.html
|
||||
share/doc/coq/html/node.2.html
|
||||
share/doc/coq/html/node.3.0.0.html
|
||||
share/doc/coq/html/node.3.0.1.html
|
||||
share/doc/coq/html/node.3.0.2.html
|
||||
share/doc/coq/html/node.3.0.3.html
|
||||
share/doc/coq/html/node.3.0.4.html
|
||||
share/doc/coq/html/node.3.0.html
|
||||
share/doc/coq/html/node.3.1.0.html
|
||||
share/doc/coq/html/node.3.1.1.html
|
||||
share/doc/coq/html/node.3.1.2.html
|
||||
share/doc/coq/html/node.3.1.3.html
|
||||
share/doc/coq/html/node.3.1.4.html
|
||||
share/doc/coq/html/node.3.1.5.html
|
||||
share/doc/coq/html/node.3.1.6.html
|
||||
share/doc/coq/html/node.3.1.7.html
|
||||
share/doc/coq/html/node.3.1.8.html
|
||||
share/doc/coq/html/node.3.1.html
|
||||
share/doc/coq/html/node.3.2.0.html
|
||||
share/doc/coq/html/node.3.2.1.html
|
||||
share/doc/coq/html/node.3.2.2.html
|
||||
share/doc/coq/html/node.3.2.3.html
|
||||
share/doc/coq/html/node.3.2.4.html
|
||||
share/doc/coq/html/node.3.2.html
|
||||
share/doc/coq/html/node.3.3.0.html
|
||||
share/doc/coq/html/node.3.3.1.html
|
||||
share/doc/coq/html/node.3.3.2.html
|
||||
share/doc/coq/html/node.3.3.3.html
|
||||
share/doc/coq/html/node.3.3.4.html
|
||||
share/doc/coq/html/node.3.3.5.html
|
||||
share/doc/coq/html/node.3.3.6.html
|
||||
share/doc/coq/html/node.3.3.7.html
|
||||
share/doc/coq/html/node.3.3.8.html
|
||||
share/doc/coq/html/node.3.3.9.html
|
||||
share/doc/coq/html/node.3.3.html
|
||||
share/doc/coq/html/node.3.4.0.html
|
||||
share/doc/coq/html/node.3.4.1.html
|
||||
share/doc/coq/html/node.3.4.2.html
|
||||
share/doc/coq/html/node.3.4.3.html
|
||||
share/doc/coq/html/node.3.4.html
|
||||
share/doc/coq/html/node.3.5.0.html
|
||||
share/doc/coq/html/node.3.5.1.html
|
||||
share/doc/coq/html/node.3.5.2.html
|
||||
share/doc/coq/html/node.3.5.3.html
|
||||
share/doc/coq/html/node.3.5.4.html
|
||||
share/doc/coq/html/node.3.5.5.html
|
||||
share/doc/coq/html/node.3.5.6.html
|
||||
share/doc/coq/html/node.3.5.html
|
||||
share/doc/coq/html/node.3.6.0.html
|
||||
share/doc/coq/html/node.3.6.1.html
|
||||
share/doc/coq/html/node.3.6.2.html
|
||||
share/doc/coq/html/node.3.6.html
|
||||
share/doc/coq/html/node.3.7.0.html
|
||||
share/doc/coq/html/node.3.7.1.html
|
||||
share/doc/coq/html/node.3.7.2.html
|
||||
share/doc/coq/html/node.3.7.3.html
|
||||
share/doc/coq/html/node.3.7.4.html
|
||||
share/doc/coq/html/node.3.7.5.html
|
||||
share/doc/coq/html/node.3.7.6.html
|
||||
share/doc/coq/html/node.3.7.7.html
|
||||
share/doc/coq/html/node.3.7.html
|
||||
share/doc/coq/html/node.3.html
|
||||
share/doc/coq/html/node.4.html
|
||||
share/doc/coq/html/node.5.html
|
||||
share/doc/coq/html/node.6.html
|
||||
share/doc/coq/html/node.7.html
|
||||
share/doc/coq/html/node.8.html
|
||||
share/doc/coq/html/node.x.0.0.html
|
||||
share/doc/coq/html/node.x.0.1.html
|
||||
share/doc/coq/html/node.x.0.html
|
||||
share/doc/coq/html/node.x.1.0.html
|
||||
share/doc/coq/html/node.x.1.1.html
|
||||
share/doc/coq/html/node.x.1.2.html
|
||||
share/doc/coq/html/node.x.1.3.html
|
||||
share/doc/coq/html/node.x.1.html
|
||||
share/doc/coq/html/prev.gif
|
||||
share/doc/coq/html/root.gif
|
||||
share/doc/coq/html/sub.gif
|
||||
share/doc/coq/html/toc.html
|
||||
share/doc/coq/html/tutorial.html
|
||||
share/doc/coq/ps/Changes.ps
|
||||
share/doc/coq/ps/Library.ps
|
||||
share/doc/coq/ps/Reference-Manual-addendum.ps
|
||||
share/doc/coq/ps/Reference-Manual-base.ps
|
||||
share/doc/coq/ps/Tutorial.ps
|
||||
share/emacs/site-lisp/coq.el
|
||||
@dirrm share/doc/coq/ps
|
||||
@dirrm share/doc/coq/html
|
||||
@dirrm share/doc/coq
|
||||
@dirrm lib/coq/theories/ZArith
|
||||
@dirrm lib/coq/theories/Wellfounded
|
||||
@dirrm lib/coq/theories/Sets
|
||||
@dirrm lib/coq/theories/Relations
|
||||
@dirrm lib/coq/theories/Reals
|
||||
@dirrm lib/coq/theories/Logic
|
||||
@dirrm lib/coq/theories/Lists
|
||||
@dirrm lib/coq/theories/IntMap
|
||||
@dirrm lib/coq/theories/Init
|
||||
@dirrm lib/coq/theories/Bool
|
||||
@dirrm lib/coq/theories/Arith
|
||||
@dirrm lib/coq/theories
|
||||
@dirrm lib/coq/tactics
|
||||
@dirrm lib/coq/states
|
||||
@dirrm lib/coq/contrib/xml
|
||||
@dirrm lib/coq/contrib/ring
|
||||
@dirrm lib/coq/contrib/omega
|
||||
@dirrm lib/coq/contrib/interface
|
||||
@dirrm lib/coq/contrib/fourier
|
||||
@dirrm lib/coq/contrib/field
|
||||
@dirrm lib/coq/contrib/extraction
|
||||
@dirrm lib/coq/contrib/correctness
|
||||
@dirrm lib/coq/contrib
|
||||
@dirrm lib/coq
|
||||
Loading…
Reference in New Issue
Block a user